Atoms, Coatoms, and Simple Lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module defines atoms, which are minimal non-⊥ elements in bounded lattices, simple lattices, which are lattices with only two elements, and related ideas.

Main definitions #

Atoms and Coatoms #

is_atom a indicates that the only element below a is ⊥.
is_coatom a indicates that the only element above a is ⊤.

Atomic and Atomistic Lattices #

is_atomic indicates that every element other than ⊥ is above an atom.
is_coatomic indicates that every element other than ⊤ is below a coatom.
is_atomistic indicates that every element is the Sup of a set of atoms.
is_coatomistic indicates that every element is the Inf of a set of coatoms.

Simple Lattices #

is_simple_order indicates that an order has only two unique elements, ⊥ and ⊤.
is_simple_order.bounded_order
is_simple_order.distrib_lattice
Given an instance of is_simple_order, we provide the following definitions. These are not made global instances as they contain data :

Main results #

is_atom_dual_iff_is_coatom and is_coatom_dual_iff_is_atom express the (definitional) duality of is_atom and is_coatom.
is_simple_order_iff_is_atom_top and is_simple_order_iff_is_coatom_bot express the connection between atoms, coatoms, and simple lattices
is_compl.is_atom_iff_is_coatom and is_compl.is_coatom_if_is_atom: In a modular bounded lattice, a complement of an atom is a coatom and vice versa.
is_atomic_iff_is_coatomic: A modular complemented lattice is atomic iff it is coatomic.

source

def is_atom {α : Type u_1} [preorder α] [order_bot α] (a : α) :

Prop

An atom of an order_bot is an element with no other element between it and ⊥, which is not ⊥.

Equations

is_atom a = (a ≠ ⊥ ∧ ∀ (b : α), b < a → b = ⊥)

source

theorem is_atom.Iic {α : Type u_1} [preorder α] [order_bot α] {a x : α} (ha : is_atom a) (hax : a ≤ x) :

is_atom ⟨a, hax⟩

source

theorem is_atom.of_is_atom_coe_Iic {α : Type u_1} [preorder α] [order_bot α] {x : α} {a : ↥(set.Iic x)} (ha : is_atom a) :

is_atom ↑a

source

theorem is_atom_iff {α : Type u_1} [preorder α] [order_bot α] {a : α} :

is_atom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b

source

theorem is_atom.lt_iff {α : Type u_1} [partial_order α] [order_bot α] {a x : α} (h : is_atom a) :

x < a ↔ x = ⊥

source

theorem is_atom.le_iff {α : Type u_1} [partial_order α] [order_bot α] {a x : α} (h : is_atom a) :

x ≤ a ↔ x = ⊥ ∨ x = a

source

theorem is_atom.Iic_eq {α : Type u_1} [partial_order α] [order_bot α] {a : α} (h : is_atom a) :

set.Iic a = {⊥, a}

source

@[simp]

theorem bot_covby_iff {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

⊥ ⋖ a ↔ is_atom a

source

theorem covby.is_atom {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

⊥ ⋖ a → is_atom a

Alias of the forward direction of bot_covby_iff.

source

theorem is_atom.bot_covby {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

is_atom a → ⊥ ⋖ a

Alias of the reverse direction of bot_covby_iff.

source

def is_coatom {α : Type u_1} [preorder α] [order_top α] (a : α) :

Prop

A coatom of an order_top is an element with no other element between it and ⊤, which is not ⊤.

Equations

is_coatom a = (a ≠ ⊤ ∧ ∀ (b : α), a < b → b = ⊤)

source

@[simp]

theorem is_coatom_dual_iff_is_atom {α : Type u_1} [preorder α] [order_bot α] {a : α} :

is_coatom (⇑order_dual.to_dual a) ↔ is_atom a

source

@[simp]

theorem is_atom_dual_iff_is_coatom {α : Type u_1} [preorder α] [order_top α] {a : α} :

is_atom (⇑order_dual.to_dual a) ↔ is_coatom a

source

theorem is_atom.dual {α : Type u_1} [preorder α] [order_bot α] {a : α} :

is_atom a → is_coatom (⇑order_dual.to_dual a)

Alias of the reverse direction of is_coatom_dual_iff_is_atom.

source

theorem is_coatom.dual {α : Type u_1} [preorder α] [order_top α] {a : α} :

is_coatom a → is_atom (⇑order_dual.to_dual a)

Alias of the reverse direction of is_atom_dual_iff_is_coatom.

source

theorem is_coatom.Ici {α : Type u_1} [preorder α] [order_top α] {a x : α} (ha : is_coatom a) (hax : x ≤ a) :

is_coatom ⟨a, hax⟩

source

theorem is_coatom.of_is_coatom_coe_Ici {α : Type u_1} [preorder α] [order_top α] {x : α} {a : ↥(set.Ici x)} (ha : is_coatom a) :

is_coatom ↑a

source

theorem is_coatom_iff {α : Type u_1} [preorder α] [order_top α] {a : α} :

is_coatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a

source

theorem is_coatom.lt_iff {α : Type u_1} [partial_order α] [order_top α] {a x : α} (h : is_coatom a) :

a < x ↔ x = ⊤

source

theorem is_coatom.le_iff {α : Type u_1} [partial_order α] [order_top α] {a x : α} (h : is_coatom a) :

a ≤ x ↔ x = ⊤ ∨ x = a

source

theorem is_coatom.Ici_eq {α : Type u_1} [partial_order α] [order_top α] {a : α} (h : is_coatom a) :

set.Ici a = {⊤, a}

source

@[simp]

theorem covby_top_iff {α : Type u_1} [partial_order α] [order_top α] {a : α} :

a ⋖ ⊤ ↔ is_coatom a

source

theorem covby.is_coatom {α : Type u_1} [partial_order α] [order_top α] {a : α} :

a ⋖ ⊤ → is_coatom a

Alias of the forward direction of covby_top_iff.

source

theorem is_coatom.covby_top {α : Type u_1} [partial_order α] [order_top α] {a : α} :

is_coatom a → a ⋖ ⊤

Alias of the reverse direction of covby_top_iff.

source

@[simp]

theorem set.Ici.is_atom_iff {α : Type u_1} [partial_order α] {a : α} {b : ↥(set.Ici a)} :

is_atom b ↔ a ⋖ ↑b

source

@[simp]

theorem set.Iic.is_coatom_iff {α : Type u_1} [partial_order α] {b : α} {a : ↥(set.Iic b)} :

is_coatom a ↔ ↑a ⋖ b

source

theorem covby_iff_atom_Ici {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :

a ⋖ b ↔ is_atom ⟨b, h⟩

source

theorem covby_iff_coatom_Iic {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :

a ⋖ b ↔ is_coatom ⟨a, h⟩

source

theorem is_atom.inf_eq_bot_of_ne {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (ha : is_atom a) (hb : is_atom b) (hab : a ≠ b) :

a ⊓ b = ⊥

source

theorem is_atom.disjoint_of_ne {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} (ha : is_atom a) (hb : is_atom b) (hab : a ≠ b) :

disjoint a b

source

theorem is_coatom.sup_eq_top_of_ne {α : Type u_1} [semilattice_sup α] [order_top α] {a b : α} (ha : is_coatom a) (hb : is_coatom b) (hab : a ≠ b) :

a ⊔ b = ⊤

source

@[class]

structure is_atomic (α : Type u_1) [partial_order α] [order_bot α] :

Prop

eq_bot_or_exists_atom_le : ∀ (b : α), b = ⊥ ∨ ∃ (a : α), is_atom a ∧ a ≤ b

A lattice is atomic iff every element other than ⊥ has an atom below it.

Instances of this typeclass

source

theorem is_atomic_iff (α : Type u_1) [partial_order α] [order_bot α] :

is_atomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ (a : α), is_atom a ∧ a ≤ b

source

@[class]

structure is_coatomic (α : Type u_1) [partial_order α] [order_top α] :

Prop

eq_top_or_exists_le_coatom : ∀ (b : α), b = ⊤ ∨ ∃ (a : α), is_coatom a ∧ b ≤ a

A lattice is coatomic iff every element other than ⊤ has a coatom above it.

Instances of this typeclass

source

theorem is_coatomic_iff (α : Type u_1) [partial_order α] [order_top α] :

is_coatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ (a : α), is_coatom a ∧ b ≤ a

source

@[simp]

theorem is_coatomic_dual_iff_is_atomic {α : Type u_1} [partial_order α] [order_bot α] :

is_coatomic αᵒᵈ ↔ is_atomic α

source

@[simp]

theorem is_atomic_dual_iff_is_coatomic {α : Type u_1} [partial_order α] [order_top α] :

is_atomic αᵒᵈ ↔ is_coatomic α

source

@[protected, instance]

def is_atomic.is_coatomic_dual {α : Type u_1} [partial_order α] [order_bot α] [is_atomic α] :

is_coatomic αᵒᵈ

source

@[protected, instance]

def is_atomic.set.Iic.is_atomic {α : Type u_1} [partial_order α] [order_bot α] [is_atomic α] {x : α} :

is_atomic ↥(set.Iic x)

source

@[protected, instance]

def is_coatomic.is_coatomic {α : Type u_1} [partial_order α] [order_top α] [is_coatomic α] :

is_atomic αᵒᵈ

source

@[protected, instance]

def is_coatomic.set.Ici.is_coatomic {α : Type u_1} [partial_order α] [order_top α] [is_coatomic α] {x : α} :

is_coatomic ↥(set.Ici x)

source

theorem is_atomic_iff_forall_is_atomic_Iic {α : Type u_1} [partial_order α] [order_bot α] :

is_atomic α ↔ ∀ (x : α), is_atomic ↥(set.Iic x)

source

theorem is_coatomic_iff_forall_is_coatomic_Ici {α : Type u_1} [partial_order α] [order_top α] :

is_coatomic α ↔ ∀ (x : α), is_coatomic ↥(set.Ici x)

source

theorem is_atomic_of_order_bot_well_founded_lt {α : Type u_1} [partial_order α] [order_bot α] (h : well_founded has_lt.lt) :

is_atomic α

source

theorem is_coatomic_of_order_top_gt_well_founded {α : Type u_1} [partial_order α] [order_top α] (h : well_founded gt) :

is_coatomic α

source

@[class]

structure is_atomistic (α : Type u_1) [complete_lattice α] :

Prop

eq_Sup_atoms : ∀ (b : α), ∃ (s : set α), b = has_Sup.Sup s ∧ ∀ (a : α), a ∈ s → is_atom a

A lattice is atomistic iff every element is a Sup of a set of atoms.

Instances of this typeclass

source

@[class]

structure is_coatomistic (α : Type u_1) [complete_lattice α] :

Prop

eq_Inf_coatoms : ∀ (b : α), ∃ (s : set α), b = has_Inf.Inf s ∧ ∀ (a : α), a ∈ s → is_coatom a

A lattice is coatomistic iff every element is an Inf of a set of coatoms.

Instances of this typeclass

source

@[simp]

theorem is_coatomistic_dual_iff_is_atomistic {α : Type u_1} [complete_lattice α] :

is_coatomistic αᵒᵈ ↔ is_atomistic α

source

@[simp]

theorem is_atomistic_dual_iff_is_coatomistic {α : Type u_1} [complete_lattice α] :

is_atomistic αᵒᵈ ↔ is_coatomistic α

source

@[protected, instance]

def is_atomistic.is_coatomistic_dual {α : Type u_1} [complete_lattice α] [h : is_atomistic α] :

is_coatomistic αᵒᵈ

source

@[protected, instance]

def is_atomistic.is_atomic {α : Type u_1} [complete_lattice α] [is_atomistic α] :

is_atomic α

source

@[simp]

theorem Sup_atoms_le_eq {α : Type u_1} [complete_lattice α] [is_atomistic α] (b : α) :

has_Sup.Sup {a : α | is_atom a ∧ a ≤ b} = b

source

@[simp]

theorem Sup_atoms_eq_top {α : Type u_1} [complete_lattice α] [is_atomistic α] :

has_Sup.Sup {a : α | is_atom a} = ⊤

source

theorem le_iff_atom_le_imp {α : Type u_1} [complete_lattice α] [is_atomistic α] {a b : α} :

a ≤ b ↔ ∀ (c : α), is_atom c → c ≤ a → c ≤ b

source

@[protected, instance]

def is_coatomistic.is_atomistic_dual {α : Type u_1} [complete_lattice α] [h : is_coatomistic α] :

is_atomistic αᵒᵈ

source

@[protected, instance]

def is_coatomistic.is_coatomic {α : Type u_1} [complete_lattice α] [is_coatomistic α] :

is_coatomic α

source

@[class]

structure is_simple_order (α : Type u_3) [has_le α] [bounded_order α] :

Prop

to_nontrivial : nontrivial α
eq_bot_or_eq_top : ∀ (a : α), a = ⊥ ∨ a = ⊤

An order is simple iff it has exactly two elements, ⊥ and ⊤.

Instances of this typeclass

source

theorem is_simple_order_iff_is_simple_order_order_dual {α : Type u_1} [has_le α] [bounded_order α] :

is_simple_order α ↔ is_simple_order αᵒᵈ

source

theorem is_simple_order.bot_ne_top {α : Type u_1} [has_le α] [bounded_order α] [is_simple_order α] :

⊥ ≠ ⊤

source

@[protected, instance]

def order_dual.is_simple_order {α : Type u_1} [has_le α] [bounded_order α] [is_simple_order α] :

is_simple_order αᵒᵈ

source

@[protected]

def is_simple_order.preorder {α : Type u_1} [has_le α] [bounded_order α] [is_simple_order α] :

preorder α

A simple bounded_order induces a preorder. This is not an instance to prevent loops.

Equations

is_simple_order.preorder = {le := has_le.le _inst_4, lt := λ (a b : α), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[protected]

def is_simple_order.linear_order {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] [decidable_eq α] :

linear_order α

A simple partial ordered bounded_order induces a linear order. This is not an instance to prevent loops.

Equations

is_simple_order.linear_order = {le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : α), dite (a = ⊥) (λ (ha : a = ⊥), decidable.is_true _) (λ (ha : ¬a = ⊥), dite (b = ⊤) (λ (hb : b = ⊤), decidable.is_true _) (λ (hb : ¬b = ⊤), decidable.is_false _)), decidable_eq := _inst_4, decidable_lt := decidable_lt_of_decidable_le (λ (a b : α), dite (a = ⊥) (λ (ha : a = ⊥), decidable.is_true _) (λ (ha : ¬a = ⊥), dite (b = ⊤) (λ (hb : b = ⊤), decidable.is_true _) (λ (hb : ¬b = ⊤), decidable.is_false _))), max := max_default (λ (a b : α), dite (a = ⊥) (λ (ha : a = ⊥), decidable.is_true _) (λ (ha : ¬a = ⊥), dite (b = ⊤) (λ (hb : b = ⊤), decidable.is_true _) (λ (hb : ¬b = ⊤), decidable.is_false _))), max_def := _, min := min_default (λ (a b : α), dite (a = ⊥) (λ (ha : a = ⊥), decidable.is_true _) (λ (ha : ¬a = ⊥), dite (b = ⊤) (λ (hb : b = ⊤), decidable.is_true _) (λ (hb : ¬b = ⊤), decidable.is_false _))), min_def := _}

source

@[simp]

theorem is_atom_top {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] :

is_atom ⊤

source

@[simp]

theorem is_coatom_bot {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] :

is_coatom ⊥

source

theorem bot_covby_top {α : Type u_1} [partial_order α] [bounded_order α] [is_simple_order α] :

⊥ ⋖ ⊤

source

theorem is_simple_order.eq_bot_of_lt {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :

a = ⊥

source

theorem is_simple_order.eq_top_of_lt {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :

b = ⊤

source

theorem is_simple_order.has_lt.lt.eq_bot {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :

a = ⊥

Alias of is_simple_order.eq_bot_of_lt.

source

theorem is_simple_order.has_lt.lt.eq_top {α : Type u_1} [preorder α] [bounded_order α] [is_simple_order α] {a b : α} (h : a < b) :

b = ⊤

Alias of is_simple_order.eq_top_of_lt.

source

@[protected]

def is_simple_order.lattice {α : Type u_1} [decidable_eq α] [partial_order α] [bounded_order α] [is_simple_order α] :

lattice α

A simple partial ordered bounded_order induces a lattice. This is not an instance to prevent loops

Equations

is_simple_order.lattice = linear_order.to_lattice

source

@[protected]

def is_simple_order.distrib_lattice {α : Type u_1} [lattice α] [bounded_order α] [is_simple_order α] :

distrib_lattice α

A lattice that is a bounded_order is a distributive lattice. This is not an instance to prevent loops

Equations

is_simple_order.distrib_lattice = {sup := lattice.sup infer_instance, le := lattice.le infer_instance, lt := lattice.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf infer_instance, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected, instance]

def is_simple_order.is_atomic {α : Type u_1} [lattice α] [bounded_order α] [is_simple_order α] :

is_atomic α

source

@[protected, instance]

def is_simple_order.is_coatomic {α : Type u_1} [lattice α] [bounded_order α] [is_simple_order α] :

is_coatomic α

source

@[simp]

theorem is_simple_order.equiv_bool_symm_apply {α : Type u_1} [decidable_eq α] [has_le α] [bounded_order α] [is_simple_order α] (x : bool) :

⇑(is_simple_order.equiv_bool.symm) x = cond x ⊤ ⊥

source

@[simp]

theorem is_simple_order.equiv_bool_apply {α : Type u_1} [decidable_eq α] [has_le α] [bounded_order α] [is_simple_order α] (x : α) :

⇑is_simple_order.equiv_bool x = decidable.to_bool (x = ⊤)

source

def is_simple_order.equiv_bool {α : Type u_1} [decidable_eq α] [has_le α] [bounded_order α] [is_simple_order α] :

α ≃ bool

Every simple lattice is isomorphic to bool, regardless of order.

Equations

is_simple_order.equiv_bool = {to_fun := λ (x : α), decidable.to_bool (x = ⊤), inv_fun := λ (x : bool), cond x ⊤ ⊥, left_inv := _, right_inv := _}

source

def is_simple_order.order_iso_bool {α : Type u_1} [decidable_eq α] [partial_order α] [bounded_order α] [is_simple_order α] :

α ≃o bool

Every simple lattice over a partial order is order-isomorphic to bool.

Equations

is_simple_order.order_iso_bool = {to_equiv := {to_fun := is_simple_order.equiv_bool.to_fun, inv_fun := is_simple_order.equiv_bool.inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[protected]

def is_simple_order.boolean_algebra {α : Type u_1} [decidable_eq α] [lattice α] [bounded_order α] [is_simple_order α] :

boolean_algebra α

A simple bounded_order is also a boolean_algebra.

Equations

is_simple_order.boolean_algebra = {sup := distrib_lattice.sup is_simple_order.distrib_lattice, le := distrib_lattice.le is_simple_order.distrib_lattice, lt := distrib_lattice.lt is_simple_order.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf is_simple_order.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := λ (x : α), ite (x = ⊥) ⊤ ⊥, sdiff := λ (x y : α), ite (x = ⊤ ∧ y = ⊥) ⊤ ⊥, himp := λ (x y : α), distrib_lattice.sup y (ite (x = ⊥) ⊤ ⊥), top := bounded_order.top (show bounded_order α, from _inst_7), bot := bounded_order.bot (show bounded_order α, from _inst_7), inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}

source

@[protected]

noncomputable def is_simple_order.complete_lattice {α : Type u_1} [lattice α] [bounded_order α] [is_simple_order α] :

complete_lattice α

A simple bounded_order is also complete.

Equations

is_simple_order.complete_lattice = {sup := lattice.sup infer_instance, le := lattice.le infer_instance, lt := lattice.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf infer_instance, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), ite (⊤ ∈ s) ⊤ ⊥, le_Sup := _, Sup_le := _, Inf := λ (s : set α), ite (⊥ ∈ s) ⊥ ⊤, Inf_le := _, le_Inf := _, top := bounded_order.top infer_instance, bot := bounded_order.bot infer_instance, le_top := _, bot_le := _}

source

@[protected]

noncomputable def is_simple_order.complete_boolean_algebra {α : Type u_1} [lattice α] [bounded_order α] [is_simple_order α] :

complete_boolean_algebra α

A simple bounded_order is also a complete_boolean_algebra.

Equations

is_simple_order.complete_boolean_algebra = {sup := complete_lattice.sup is_simple_order.complete_lattice, le := complete_lattice.le is_simple_order.complete_lattice, lt := complete_lattice.lt is_simple_order.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf is_simple_order.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := boolean_algebra.compl is_simple_order.boolean_algebra, sdiff := boolean_algebra.sdiff is_simple_order.boolean_algebra, himp := boolean_algebra.himp is_simple_order.boolean_algebra, top := complete_lattice.top is_simple_order.complete_lattice, bot := complete_lattice.bot is_simple_order.complete_lattice, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _, Sup := complete_lattice.Sup is_simple_order.complete_lattice, le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf is_simple_order.complete_lattice, Inf_le := _, le_Inf := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

source

@[protected, instance]

def is_simple_order.is_atomistic {α : Type u_1} [complete_lattice α] [is_simple_order α] :

is_atomistic α

source

@[protected, instance]

def is_simple_order.is_coatomistic {α : Type u_1} [complete_lattice α] [is_simple_order α] :

is_coatomistic α

source

theorem is_simple_order_iff_is_atom_top {α : Type u_1} [partial_order α] [bounded_order α] :

is_simple_order α ↔ is_atom ⊤

source

theorem is_simple_order_iff_is_coatom_bot {α : Type u_1} [partial_order α] [bounded_order α] :

is_simple_order α ↔ is_coatom ⊥

source

theorem set.is_simple_order_Iic_iff_is_atom {α : Type u_1} [partial_order α] [order_bot α] {a : α} :

is_simple_order ↥(set.Iic a) ↔ is_atom a

source

theorem set.is_simple_order_Ici_iff_is_coatom {α : Type u_1} [partial_order α] [order_top α] {a : α} :

is_simple_order ↥(set.Ici a) ↔ is_coatom a

source

theorem order_embedding.is_atom_of_map_bot_of_image {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] (f : β ↪o α) (hbot : ⇑f ⊥ = ⊥) {b : β} (hb : is_atom (⇑f b)) :

is_atom b

source

theorem order_embedding.is_coatom_of_map_top_of_image {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] (f : β ↪o α) (htop : ⇑f ⊤ = ⊤) {b : β} (hb : is_coatom (⇑f b)) :

is_coatom b

source

theorem galois_insertion.is_atom_of_u_bot {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] {l : α → β} {u : β → α} (gi : galois_insertion l u) (hbot : u ⊥ = ⊥) {b : β} (hb : is_atom (u b)) :

is_atom b

source

theorem galois_insertion.is_atom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [is_atomic α] [order_bot β] {l : α → β} {u : β → α} (gi : galois_insertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), is_atom a → u (l a) = a) (a : α) :

is_atom (l a) ↔ is_atom a

source

theorem galois_insertion.is_atom_iff' {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [is_atomic α] [order_bot β] {l : α → β} {u : β → α} (gi : galois_insertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ (a : α), is_atom a → u (l a) = a) (b : β) :

is_atom (u b) ↔ is_atom b

source

theorem galois_insertion.is_coatom_of_image {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] {l : α → β} {u : β → α} (gi : galois_insertion l u) {b : β} (hb : is_coatom (u b)) :

is_coatom b

source

theorem galois_insertion.is_coatom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [is_coatomic α] [order_top β] {l : α → β} {u : β → α} (gi : galois_insertion l u) (h_coatom : ∀ (a : α), is_coatom a → u (l a) = a) (b : β) :

is_coatom (u b) ↔ is_coatom b

source

theorem galois_coinsertion.is_coatom_of_l_top {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] {l : α → β} {u : β → α} (gi : galois_coinsertion l u) (hbot : l ⊤ = ⊤) {a : α} (hb : is_coatom (l a)) :

is_coatom a

source

theorem galois_coinsertion.is_coatom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] [is_coatomic β] {l : α → β} {u : β → α} (gi : galois_coinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), is_coatom b → l (u b) = b) (b : β) :

is_coatom (u b) ↔ is_coatom b

source

theorem galois_coinsertion.is_coatom_iff' {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] [is_coatomic β] {l : α → β} {u : β → α} (gi : galois_coinsertion l u) (htop : l ⊤ = ⊤) (h_coatom : ∀ (b : β), is_coatom b → l (u b) = b) (a : α) :

is_coatom (l a) ↔ is_coatom a

source

theorem galois_coinsertion.is_atom_of_image {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] {l : α → β} {u : β → α} (gi : galois_coinsertion l u) {a : α} (hb : is_atom (l a)) :

is_atom a

source

theorem galois_coinsertion.is_atom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] [is_atomic β] {l : α → β} {u : β → α} (gi : galois_coinsertion l u) (h_atom : ∀ (b : β), is_atom b → l (u b) = b) (a : α) :

is_atom (l a) ↔ is_atom a

source

@[simp]

theorem order_iso.is_atom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] (f : α ≃o β) (a : α) :

is_atom (⇑f a) ↔ is_atom a

source

@[simp]

theorem order_iso.is_coatom_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] (f : α ≃o β) (a : α) :

is_coatom (⇑f a) ↔ is_coatom a

source

theorem order_iso.is_simple_order_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [bounded_order α] [bounded_order β] (f : α ≃o β) :

is_simple_order α ↔ is_simple_order β

source

theorem order_iso.is_simple_order {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [bounded_order α] [bounded_order β] [h : is_simple_order β] (f : α ≃o β) :

is_simple_order α

source

@[protected]

theorem order_iso.is_atomic_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_bot α] [order_bot β] (f : α ≃o β) :

is_atomic α ↔ is_atomic β

source

@[protected]

theorem order_iso.is_coatomic_iff {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [order_top α] [order_top β] (f : α ≃o β) :

is_coatomic α ↔ is_coatomic β

source

theorem is_compl.is_atom_iff_is_coatom {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] {a b : α} (hc : is_compl a b) :

is_atom a ↔ is_coatom b

source

theorem is_compl.is_coatom_iff_is_atom {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] {a b : α} (hc : is_compl a b) :

is_coatom a ↔ is_atom b

source

theorem is_coatomic_of_is_atomic_of_complemented_lattice_of_is_modular {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] [complemented_lattice α] [is_atomic α] :

is_coatomic α

source

theorem is_atomic_of_is_coatomic_of_complemented_lattice_of_is_modular {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] [complemented_lattice α] [is_coatomic α] :

is_atomic α

source

theorem is_atomic_iff_is_coatomic {α : Type u_1} [lattice α] [bounded_order α] [is_modular_lattice α] [complemented_lattice α] :

is_atomic α ↔ is_coatomic α

source

theorem set.is_atom_singleton {α : Type u_1} (x : α) :

is_atom {x}

source

theorem set.is_atom_iff {α : Type u_1} (s : set α) :

is_atom s ↔ ∃ (x : α), s = {x}

source

theorem set.is_coatom_iff {α : Type u_1} (s : set α) :

is_coatom s ↔ ∃ (x : α), s = {x}ᶜ

source

theorem set.is_coatom_singleton_compl {α : Type u_1} (x : α) :

is_coatom {x}ᶜ

source

@[protected, instance]

def set.is_atomistic {α : Type u_1} :

is_atomistic (set α)

source

@[protected, instance]

def set.is_coatomistic {α : Type u_1} :

is_coatomistic (set α)