Mathlib.Order.Disjoint

Disjoint definition

(a b : α) : Prop

Full source

/-- Two elements of a lattice are disjoint if their inf is the bottom element.
  (This generalizes disjoint sets, viewed as members of the subset lattice.)

Note that we define this without reference to `⊓`, as this allows us to talk about orders where
the infimum is not unique, or where implementing `Inf` would require additional `Decidable`
arguments. -/
def Disjoint (a b : α) : Prop :=
  ∀ ⦃x⦄, x ≤ a → x ≤ b → x ≤ ⊥

Disjoint elements in a lattice

Informal description

Two elements $a$ and $b$ in a lattice with a bottom element $\bot$ are called *disjoint* if every element $x$ that is less than or equal to both $a$ and $b$ must also be less than or equal to $\bot$. This generalizes the notion of disjoint sets when viewing them as elements of the subset lattice.

disjoint_of_subsingleton theorem

[Subsingleton α] : Disjoint a b

Full source

@[simp]
theorem disjoint_of_subsingleton [Subsingleton α] : Disjoint a b :=
  fun x _ _ ↦ le_of_eq (Subsingleton.elim x ⊥)

Disjointness in Subsingleton Lattices

Informal description

In a lattice $\alpha$ with a bottom element $\bot$, if $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), then any two elements $a$ and $b$ in $\alpha$ are disjoint.

disjoint_comm theorem

: Disjoint a b ↔ Disjoint b a

Full source

theorem disjoint_comm : DisjointDisjoint a b ↔ Disjoint b a :=
  forall_congr' fun _ ↦ forall_swap

Symmetry of Disjointness in a Lattice

Informal description

For any two elements $a$ and $b$ in a lattice with a bottom element $\bot$, the statement that $a$ and $b$ are disjoint is equivalent to the statement that $b$ and $a$ are disjoint. In other words, the disjointness relation is symmetric.

Disjoint.symm theorem

⦃a b : α⦄ : Disjoint a b → Disjoint b a

Full source

@[symm]
theorem Disjoint.symm ⦃a b : α⦄ : Disjoint a b → Disjoint b a :=
  disjoint_comm.1

Symmetry of Disjointness in a Lattice

Informal description

For any two elements $a$ and $b$ in a lattice with a bottom element $\bot$, if $a$ and $b$ are disjoint, then $b$ and $a$ are also disjoint.

symmetric_disjoint theorem

: Symmetric (Disjoint : α → α → Prop)

Full source

theorem symmetric_disjoint : Symmetric (Disjoint : α → α → Prop) :=
  Disjoint.symm

Symmetry of the Disjointness Relation

Informal description

The disjointness relation `Disjoint` on a lattice with a bottom element is symmetric, meaning that for any two elements $a$ and $b$, if $a$ is disjoint with $b$, then $b$ is disjoint with $a$.

disjoint_bot_left theorem

: Disjoint ⊥ a

Full source

@[simp]
theorem disjoint_bot_left : Disjoint ⊥ a := fun _ hbot _ ↦ hbot

Bottom Element is Disjoint with Any Element

Informal description

In a lattice with a bottom element $\bot$, the bottom element is disjoint with any element $a$, i.e., $\bot \sqcap a = \bot$.

disjoint_bot_right theorem

: Disjoint a ⊥

Full source

@[simp]
theorem disjoint_bot_right : Disjoint a ⊥ := fun _ _ hbot ↦ hbot

Any Element is Disjoint with Bottom Element

Informal description

In a lattice with a bottom element $\bot$, any element $a$ is disjoint with $\bot$, i.e., $a \sqcap \bot = \bot$.

Disjoint.mono theorem

(h₁ : a ≤ b) (h₂ : c ≤ d) : Disjoint b d → Disjoint a c

Full source

theorem Disjoint.mono (h₁ : a ≤ b) (h₂ : c ≤ d) : Disjoint b d → Disjoint a c :=
  fun h _ ha hc ↦ h (ha.trans h₁) (hc.trans h₂)

Monotonicity of Disjointness in a Lattice

Informal description

Let $a, b, c, d$ be elements in a lattice with a bottom element $\bot$. If $a \leq b$ and $c \leq d$, then the disjointness of $b$ and $d$ implies the disjointness of $a$ and $c$, i.e., $b \sqcap d = \bot \implies a \sqcap c = \bot$.

Disjoint.mono_left theorem

(h : a ≤ b) : Disjoint b c → Disjoint a c

Full source

theorem Disjoint.mono_left (h : a ≤ b) : Disjoint b c → Disjoint a c :=
  Disjoint.mono h le_rfl

Left Monotonicity of Disjointness in a Lattice

Informal description

Let $a, b, c$ be elements in a lattice with a bottom element $\bot$. If $a \leq b$ and $b$ is disjoint from $c$ (i.e., $b \sqcap c = \bot$), then $a$ is also disjoint from $c$ (i.e., $a \sqcap c = \bot$).

Disjoint.mono_right theorem

: b ≤ c → Disjoint a c → Disjoint a b

Full source

theorem Disjoint.mono_right : b ≤ c → Disjoint a c → Disjoint a b :=
  Disjoint.mono le_rfl

Right Monotonicity of Disjointness in a Lattice

Informal description

Let $a, b, c$ be elements in a lattice with a bottom element $\bot$. If $b \leq c$ and $a$ is disjoint from $c$ (i.e., $a \sqcap c = \bot$), then $a$ is also disjoint from $b$ (i.e., $a \sqcap b = \bot$).

disjoint_self theorem

: Disjoint a a ↔ a = ⊥

Full source

@[simp]
theorem disjoint_self : DisjointDisjoint a a ↔ a = ⊥ :=
  ⟨fun hd ↦ bot_unique <| hd le_rfl le_rfl, fun h _ ha _ ↦ ha.trans_eq h⟩

Self-Disjointness Equivalence: $a \sqcap a = \bot \Leftrightarrow a = \bot$

Informal description

An element $a$ in a lattice with a bottom element $\bot$ is disjoint from itself if and only if $a = \bot$.

Disjoint.ne theorem

(ha : a ≠ ⊥) (hab : Disjoint a b) : a ≠ b

Full source

theorem Disjoint.ne (ha : a ≠ ⊥) (hab : Disjoint a b) : a ≠ b :=
  fun h ↦ ha <| disjoint_self.1 <| by rwa [← h] at hab

Non-Equality of Disjoint Non-Bottom Elements in a Lattice

Informal description

For any elements $a$ and $b$ in a lattice with a bottom element $\bot$, if $a$ is not equal to $\bot$ and $a$ is disjoint from $b$, then $a$ is not equal to $b$.

Disjoint.ne_iff theorem

(hab : Disjoint a b) : a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥

Full source

lemma Disjoint.ne_iff (hab : Disjoint a b) : a ≠ ba ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥ :=
  hab.eq_iff.not.trans not_and_or

Disjoint Elements Inequality Criterion: $a \neq b \leftrightarrow a \neq \bot \lor b \neq \bot$

Informal description

For any two disjoint elements $a$ and $b$ in a lattice with a bottom element $\bot$, the statement $a \neq b$ is equivalent to $a \neq \bot$ or $b \neq \bot$.

disjoint_of_le_iff_left_eq_bot theorem

(h : a ≤ b) : Disjoint a b ↔ a = ⊥

Full source

theorem disjoint_of_le_iff_left_eq_bot (h : a ≤ b) :
    DisjointDisjoint a b ↔ a = ⊥ :=
  ⟨fun hd ↦ hd.eq_bot_of_le h, fun h ↦ h ▸ disjoint_bot_left⟩

Disjointness Criterion for Elements with $a \leq b$: $a \sqcap b = \bot \leftrightarrow a = \bot$

Informal description

For any elements $a$ and $b$ in a lattice with a bottom element $\bot$, if $a \leq b$, then $a$ and $b$ are disjoint if and only if $a = \bot$.

disjoint_top theorem

: Disjoint a ⊤ ↔ a = ⊥

Full source

@[simp]
theorem disjoint_top : DisjointDisjoint a ⊤ ↔ a = ⊥ :=
  ⟨fun h ↦ bot_unique <| h le_rfl le_top, fun h _ ha _ ↦ ha.trans_eq h⟩

Disjointness with Top Element: $a \sqcap \top = \bot \leftrightarrow a = \bot$

Informal description

For any element $a$ in a bounded lattice, $a$ is disjoint with the top element $\top$ if and only if $a$ is equal to the bottom element $\bot$.

top_disjoint theorem

: Disjoint ⊤ a ↔ a = ⊥

Full source

@[simp]
theorem top_disjoint : DisjointDisjoint ⊤ a ↔ a = ⊥ :=
  ⟨fun h ↦ bot_unique <| h le_top le_rfl, fun h _ _ ha ↦ ha.trans_eq h⟩

Disjointness with Top Element: $\top \sqcap a = \bot \leftrightarrow a = \bot$

Informal description

For any element $a$ in a bounded lattice with top element $\top$ and bottom element $\bot$, the elements $\top$ and $a$ are disjoint if and only if $a = \bot$.

disjoint_iff_inf_le theorem

: Disjoint a b ↔ a ⊓ b ≤ ⊥

Full source

theorem disjoint_iff_inf_le : DisjointDisjoint a b ↔ a ⊓ b ≤ ⊥ :=
  ⟨fun hd ↦ hd inf_le_left inf_le_right, fun h _ ha hb ↦ (le_inf ha hb).trans h⟩

Disjointness Criterion via Infimum: $a \sqcap b \leq \bot$

Informal description

Two elements $a$ and $b$ in a meet-semilattice with a bottom element $\bot$ are disjoint if and only if their infimum $a \sqcap b$ is less than or equal to $\bot$.

disjoint_iff theorem

: Disjoint a b ↔ a ⊓ b = ⊥

Full source

theorem disjoint_iff : DisjointDisjoint a b ↔ a ⊓ b = ⊥ :=
  disjoint_iff_inf_le.trans le_bot_iff

Disjointness Criterion: $a \sqcap b = \bot$

Informal description

Two elements $a$ and $b$ in a meet-semilattice with a bottom element $\bot$ are disjoint if and only if their infimum $a \sqcap b$ equals $\bot$.

Disjoint.le_bot theorem

: Disjoint a b → a ⊓ b ≤ ⊥

Full source

theorem Disjoint.le_bot : Disjoint a b → a ⊓ b ≤ ⊥ :=
  disjoint_iff_inf_le.mp

Disjoint Elements Have Infimum Below Bottom

Informal description

For any two elements $a$ and $b$ in a meet-semilattice with a bottom element $\bot$, if $a$ and $b$ are disjoint, then their infimum $a \sqcap b$ is less than or equal to $\bot$.

disjoint_assoc theorem

: Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Full source

theorem disjoint_assoc : DisjointDisjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c) := by
  rw [disjoint_iff_inf_le, disjoint_iff_inf_le, inf_assoc]

Associativity of Disjointness in Meet-Semilattices

Informal description

For elements $a, b, c$ in a meet-semilattice with a bottom element $\bot$, the elements $(a \sqcap b)$ and $c$ are disjoint if and only if $a$ and $(b \sqcap c)$ are disjoint. In other words, $$(a \sqcap b) \sqcap c \leq \bot \Leftrightarrow a \sqcap (b \sqcap c) \leq \bot.$$

disjoint_left_comm theorem

: Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Full source

theorem disjoint_left_comm : DisjointDisjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c) := by
  simp_rw [disjoint_iff_inf_le, inf_left_comm]

Left Commutativity of Disjointness in Meet-Semilattices

Informal description

For elements $a, b, c$ in a meet-semilattice with a bottom element $\bot$, the element $a$ is disjoint from $b \sqcap c$ if and only if $b$ is disjoint from $a \sqcap c$. In other words, $$a \sqcap (b \sqcap c) = \bot \Leftrightarrow b \sqcap (a \sqcap c) = \bot.$$

disjoint_right_comm theorem

: Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Full source

theorem disjoint_right_comm : DisjointDisjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b := by
  simp_rw [disjoint_iff_inf_le, inf_right_comm]

Right Commutativity of Disjointness in Meet-Semilattices

Informal description

For elements $a, b, c$ in a meet-semilattice with a bottom element $\bot$, the elements $(a \sqcap b)$ and $c$ are disjoint if and only if the elements $(a \sqcap c)$ and $b$ are disjoint. In other words, $$(a \sqcap b) \sqcap c \leq \bot \Leftrightarrow (a \sqcap c) \sqcap b \leq \bot.$$

Disjoint.inf_left theorem

(h : Disjoint a b) : Disjoint (a ⊓ c) b

Full source

theorem Disjoint.inf_left (h : Disjoint a b) : Disjoint (a ⊓ c) b :=
  h.mono_left inf_le_left

Disjointness Preservation Under Left Infimum

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then the infimum of $a$ and $c$ is also disjoint from $b$ (i.e., $(a \sqcap c) \sqcap b = \bot$).

Disjoint.inf_left' theorem

(h : Disjoint a b) : Disjoint (c ⊓ a) b

Full source

theorem Disjoint.inf_left' (h : Disjoint a b) : Disjoint (c ⊓ a) b :=
  h.mono_left inf_le_right

Left Meet Preserves Disjointness

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then for any element $c$, the elements $c \sqcap a$ and $b$ are also disjoint (i.e., $(c \sqcap a) \sqcap b = \bot$).

Disjoint.inf_right theorem

(h : Disjoint a b) : Disjoint a (b ⊓ c)

Full source

theorem Disjoint.inf_right (h : Disjoint a b) : Disjoint a (b ⊓ c) :=
  h.mono_right inf_le_left

Disjointness Preservation Under Right Infimum

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then $a$ is also disjoint with $b \sqcap c$ (i.e., $a \sqcap (b \sqcap c) = \bot$).

Disjoint.inf_right' theorem

(h : Disjoint a b) : Disjoint a (c ⊓ b)

Full source

theorem Disjoint.inf_right' (h : Disjoint a b) : Disjoint a (c ⊓ b) :=
  h.mono_right inf_le_right

Disjointness Preservation under Right Infimum: $a \perp b \implies a \perp (c \sqcap b)$

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then $a$ is also disjoint with the infimum of $c$ and $b$ (i.e., $a \sqcap (c \sqcap b) = \bot$).

Disjoint.of_disjoint_inf_of_le theorem

(h : Disjoint (a ⊓ b) c) (hle : a ≤ c) : Disjoint a b

Full source

theorem Disjoint.of_disjoint_inf_of_le (h : Disjoint (a ⊓ b) c) (hle : a ≤ c) : Disjoint a b :=
  disjoint_iff.2 <| h.eq_bot_of_le <| inf_le_of_left_le hle

Disjointness from Infimum and Order Relation: $a \sqcap b \perp c \land a \leq c \implies a \perp b$

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If the infimum $a \sqcap b$ is disjoint with $c$ (i.e., $(a \sqcap b) \sqcap c = \bot$) and $a \leq c$, then $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

Disjoint.of_disjoint_inf_of_le' theorem

(h : Disjoint (a ⊓ b) c) (hle : b ≤ c) : Disjoint a b

Full source

theorem Disjoint.of_disjoint_inf_of_le' (h : Disjoint (a ⊓ b) c) (hle : b ≤ c) : Disjoint a b :=
  disjoint_iff.2 <| h.eq_bot_of_le <| inf_le_of_right_le hle

Disjointness from Infimum and Order Condition: $a \perp b$ via $(a \sqcap b) \perp c$ and $b \leq c$

Informal description

Let $a$, $b$, and $c$ be elements in a meet-semilattice with a bottom element $\bot$. If the infimum $a \sqcap b$ is disjoint from $c$ (i.e., $(a \sqcap b) \sqcap c = \bot$) and $b \leq c$, then $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

Disjoint.right_lt_sup_of_left_ne_bot theorem

[SemilatticeSup α] [OrderBot α] {a b : α} (h : Disjoint a b) (ha : a ≠ ⊥) : b < a ⊔ b

Full source

theorem Disjoint.right_lt_sup_of_left_ne_bot [SemilatticeSup α] [OrderBot α] {a b : α}
    (h : Disjoint a b) (ha : a ≠ ⊥) : b < a ⊔ b :=
  le_sup_right.lt_of_ne fun eq ↦ ha (le_bot_iff.mp <| h le_rfl <| sup_eq_right.mp eq.symm)

Strict Supremum Inequality for Disjoint Elements with Non-Bottom Left Operand

Informal description

Let $\alpha$ be a join-semilattice with a bottom element $\bot$. For any two elements $a, b \in \alpha$ such that $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$) and $a \neq \bot$, we have $b < a \sqcup b$.

disjoint_sup_left theorem

: Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Full source

@[simp]
theorem disjoint_sup_left : DisjointDisjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c := by
  simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

Disjointness of Join: $(a \sqcup b) \perp c \leftrightarrow a \perp c \text{ and } b \perp c$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a bottom element $\bot$, the join $a \sqcup b$ is disjoint from $c$ if and only if both $a$ and $b$ are disjoint from $c$ individually. That is: $$ (a \sqcup b) \sqcap c = \bot \quad \text{if and only if} \quad a \sqcap c = \bot \text{ and } b \sqcap c = \bot. $$

disjoint_sup_right theorem

: Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Full source

@[simp]
theorem disjoint_sup_right : DisjointDisjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c := by
  simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

Disjointness is Preserved Under Joins: $a \sqcap (b \sqcup c) = \bot \leftrightarrow (a \sqcap b = \bot) \land (a \sqcap c = \bot)$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a bottom element $\bot$, the element $a$ is disjoint from the join $b \sqcup c$ if and only if $a$ is disjoint from both $b$ and $c$ individually. In other words: $$ a \sqcap (b \sqcup c) = \bot \quad \text{if and only if} \quad a \sqcap b = \bot \text{ and } a \sqcap c = \bot. $$

Disjoint.sup_left theorem

(ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ⊔ b) c

Full source

theorem Disjoint.sup_left (ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ⊔ b) c :=
  disjoint_sup_left.2 ⟨ha, hb⟩

Disjointness Preserved Under Join: $a \perp c \land b \perp c \to (a \sqcup b) \perp c$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a bottom element $\bot$, if $a$ is disjoint from $c$ (i.e., $a \sqcap c = \bot$) and $b$ is disjoint from $c$ (i.e., $b \sqcap c = \bot$), then their join $a \sqcup b$ is also disjoint from $c$ (i.e., $(a \sqcup b) \sqcap c = \bot$).

Disjoint.sup_right theorem

(hb : Disjoint a b) (hc : Disjoint a c) : Disjoint a (b ⊔ c)

Full source

theorem Disjoint.sup_right (hb : Disjoint a b) (hc : Disjoint a c) : Disjoint a (b ⊔ c) :=
  disjoint_sup_right.2 ⟨hb, hc⟩

Disjointness Preserved Under Join: $a \sqcap b = \bot \land a \sqcap c = \bot \to a \sqcap (b \sqcup c) = \bot$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a bottom element $\bot$, if $a$ is disjoint from $b$ (i.e., $a \sqcap b = \bot$) and $a$ is disjoint from $c$ (i.e., $a \sqcap c = \bot$), then $a$ is also disjoint from the join $b \sqcup c$ (i.e., $a \sqcap (b \sqcup c) = \bot$).

Disjoint.left_le_of_le_sup_right theorem

(h : a ≤ b ⊔ c) (hd : Disjoint a c) : a ≤ b

Full source

theorem Disjoint.left_le_of_le_sup_right (h : a ≤ b ⊔ c) (hd : Disjoint a c) : a ≤ b :=
  le_of_inf_le_sup_le (le_trans hd.le_bot bot_le) <| sup_le h le_sup_right

Disjointness Implication: $a \leq b \sqcup c$ and $a \sqcap c \leq \bot$ implies $a \leq b$

Informal description

In a lattice with a bottom element $\bot$, if $a \leq b \sqcup c$ and $a$ is disjoint from $c$ (i.e., $a \sqcap c \leq \bot$), then $a \leq b$.

Disjoint.left_le_of_le_sup_left theorem

(h : a ≤ c ⊔ b) (hd : Disjoint a c) : a ≤ b

Full source

theorem Disjoint.left_le_of_le_sup_left (h : a ≤ c ⊔ b) (hd : Disjoint a c) : a ≤ b :=
  hd.left_le_of_le_sup_right <| by rwa [sup_comm]

Disjointness Implication: $a \leq c \sqcup b$ and $a \sqcap c \leq \bot$ implies $a \leq b$

Informal description

In a lattice with a bottom element $\bot$, if $a \leq c \sqcup b$ and $a$ is disjoint from $c$ (i.e., $a \sqcap c \leq \bot$), then $a \leq b$.

Codisjoint definition

(a b : α) : Prop

Full source

/-- Two elements of a lattice are codisjoint if their sup is the top element.

Note that we define this without reference to `⊔`, as this allows us to talk about orders where
the supremum is not unique, or where implement `Sup` would require additional `Decidable`
arguments. -/
def Codisjoint (a b : α) : Prop :=
  ∀ ⦃x⦄, a ≤ x → b ≤ x → ⊤ ≤ x

Codisjoint elements in a lattice

Informal description

Two elements $ a $ and $ b $ of a lattice $ \alpha $ with a top element $ \top $ are called *codisjoint* if for any element $ x $, whenever $ a \leq x $ and $ b \leq x $, then $ \top \leq x $. This is equivalent to saying that the supremum of $ a $ and $ b $ is $ \top $, but the definition avoids direct reference to the supremum operation.

codisjoint_comm theorem

: Codisjoint a b ↔ Codisjoint b a

Full source

theorem codisjoint_comm : CodisjointCodisjoint a b ↔ Codisjoint b a :=
  forall_congr' fun _ ↦ forall_swap

Symmetry of Codisjointness Relation

Informal description

Two elements $a$ and $b$ in a lattice with a top element are codisjoint if and only if $b$ and $a$ are codisjoint. In other words, the codisjointness relation is symmetric.

Codisjoint.symm theorem

⦃a b : α⦄ : Codisjoint a b → Codisjoint b a

Full source

@[symm]
theorem Codisjoint.symm ⦃a b : α⦄ : Codisjoint a b → Codisjoint b a :=
  codisjoint_comm.1

Symmetry of Codisjointness

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with a top element $\top$, if $a$ and $b$ are codisjoint, then $b$ and $a$ are also codisjoint.

symmetric_codisjoint theorem

: Symmetric (Codisjoint : α → α → Prop)

Full source

theorem symmetric_codisjoint : Symmetric (Codisjoint : α → α → Prop) :=
  Codisjoint.symm

Symmetry of Codisjointness Relation

Informal description

The relation of codisjointness is symmetric in any lattice $\alpha$ with a top element $\top$. That is, for any two elements $a, b \in \alpha$, if $a$ and $b$ are codisjoint, then $b$ and $a$ are also codisjoint.

codisjoint_top_left theorem

: Codisjoint ⊤ a

Full source

@[simp]
theorem codisjoint_top_left : Codisjoint ⊤ a := fun _ htop _ ↦ htop

Top Element is Codisjoint with Any Element

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the elements $\top$ and $a$ are codisjoint.

codisjoint_top_right theorem

: Codisjoint a ⊤

Full source

@[simp]
theorem codisjoint_top_right : Codisjoint a ⊤ := fun _ _ htop ↦ htop

Any Element is Codisjoint with Top Element

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the elements $a$ and $\top$ are codisjoint, meaning their join is equal to $\top$.

Codisjoint.mono theorem

(h₁ : a ≤ b) (h₂ : c ≤ d) : Codisjoint a c → Codisjoint b d

Full source

theorem Codisjoint.mono (h₁ : a ≤ b) (h₂ : c ≤ d) : Codisjoint a c → Codisjoint b d :=
  fun h _ ha hc ↦ h (h₁.trans ha) (h₂.trans hc)

Monotonicity of Codisjointness under Order Relations

Informal description

Let $ a, b, c, d $ be elements of a lattice $ \alpha $ with a top element $ \top $. If $ a \leq b $ and $ c \leq d $, and $ a $ and $ c $ are codisjoint (i.e., their join is $ \top $), then $ b $ and $ d $ are also codisjoint.

Codisjoint.mono_left theorem

(h : a ≤ b) : Codisjoint a c → Codisjoint b c

Full source

theorem Codisjoint.mono_left (h : a ≤ b) : Codisjoint a c → Codisjoint b c :=
  Codisjoint.mono h le_rfl

Left Monotonicity of Codisjointness

Informal description

Let $a$, $b$, and $c$ be elements of a lattice $\alpha$ with a top element $\top$. If $a \leq b$ and $a$ and $c$ are codisjoint (i.e., their join is $\top$), then $b$ and $c$ are also codisjoint.

Codisjoint.mono_right theorem

: b ≤ c → Codisjoint a b → Codisjoint a c

Full source

theorem Codisjoint.mono_right : b ≤ c → Codisjoint a b → Codisjoint a c :=
  Codisjoint.mono le_rfl

Right Monotonicity of Codisjointness

Informal description

Let $a$, $b$, and $c$ be elements of a lattice $\alpha$ with a top element $\top$. If $b \leq c$ and $a$ and $b$ are codisjoint (i.e., their join is $\top$), then $a$ and $c$ are also codisjoint.

codisjoint_self theorem

: Codisjoint a a ↔ a = ⊤

Full source

@[simp]
theorem codisjoint_self : CodisjointCodisjoint a a ↔ a = ⊤ :=
  ⟨fun hd ↦ top_unique <| hd le_rfl le_rfl, fun h _ ha _ ↦ h.symm.trans_le ha⟩

Self-Codisjointness Equivalence: $\text{Codisjoint}(a, a) \leftrightarrow a = \top$

Informal description

An element $a$ in a lattice with a top element $\top$ is codisjoint with itself if and only if $a = \top$. In other words, the supremum of $a$ with itself is $\top$ precisely when $a$ is the top element.

Codisjoint.ne theorem

(ha : a ≠ ⊤) (hab : Codisjoint a b) : a ≠ b

Full source

theorem Codisjoint.ne (ha : a ≠ ⊤) (hab : Codisjoint a b) : a ≠ b :=
  fun h ↦ ha <| codisjoint_self.1 <| by rwa [← h] at hab

Non-Equality of Non-Top Codisjoint Elements

Informal description

For any elements $a$ and $b$ in a lattice with a top element $\top$, if $a \neq \top$ and $a$ and $b$ are codisjoint, then $a \neq b$.

Codisjoint.ne_iff theorem

(hab : Codisjoint a b) : a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤

Full source

lemma Codisjoint.ne_iff (hab : Codisjoint a b) : a ≠ ba ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤ :=
  hab.eq_iff.not.trans not_and_or

Inequality of Codisjoint Elements in Terms of Top Element

Informal description

Let $a$ and $b$ be codisjoint elements in a lattice with a top element $\top$. Then $a \neq b$ if and only if either $a \neq \top$ or $b \neq \top$.

codisjoint_bot theorem

: Codisjoint a ⊥ ↔ a = ⊤

Full source

@[simp]
theorem codisjoint_bot : CodisjointCodisjoint a ⊥ ↔ a = ⊤ :=
  ⟨fun h ↦ top_unique <| h le_rfl bot_le, fun h _ ha _ ↦ h.symm.trans_le ha⟩

Characterization of codisjointness with bottom: $a \sqcup \bot = \top \leftrightarrow a = \top$

Informal description

In a bounded lattice with top element $\top$ and bottom element $\bot$, an element $a$ is codisjoint with $\bot$ if and only if $a = \top$.

bot_codisjoint theorem

: Codisjoint ⊥ a ↔ a = ⊤

Full source

@[simp]
theorem bot_codisjoint : CodisjointCodisjoint ⊥ a ↔ a = ⊤ :=
  ⟨fun h ↦ top_unique <| h bot_le le_rfl, fun h _ _ ha ↦ h.symm.trans_le ha⟩

Bottom Element is Codisjoint with $a$ iff $a$ is Top Element

Informal description

In a bounded lattice with bottom element $\bot$ and top element $\top$, the elements $\bot$ and $a$ are codisjoint if and only if $a = \top$.

Codisjoint.ne_bot_of_ne_top theorem

(h : Codisjoint a b) (ha : a ≠ ⊤) : b ≠ ⊥

Full source

lemma Codisjoint.ne_bot_of_ne_top (h : Codisjoint a b) (ha : a ≠ ⊤) : b ≠ ⊥ := by
  rintro rfl; exact ha <| by simpa using h

Non-top codisjoint element implies non-bottom complement

Informal description

Let $a$ and $b$ be elements of a bounded lattice $\alpha$ with top element $\top$ and bottom element $\bot$. If $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$) and $a \neq \top$, then $b \neq \bot$.

Codisjoint.ne_bot_of_ne_top' theorem

(h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥

Full source

lemma Codisjoint.ne_bot_of_ne_top' (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥ := by
  rintro rfl; exact hb <| by simpa using h

Non-top codisjoint element implies non-bottom complement

Informal description

Let $a$ and $b$ be elements of a bounded lattice $\alpha$ with top element $\top$ and bottom element $\bot$. If $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$) and $b \neq \top$, then $a \neq \bot$.

codisjoint_iff_le_sup theorem

: Codisjoint a b ↔ ⊤ ≤ a ⊔ b

Full source

theorem codisjoint_iff_le_sup : CodisjointCodisjoint a b ↔ ⊤ ≤ a ⊔ b :=
  @disjoint_iff_inf_le αᵒᵈ _ _ _ _

Codisjointness Criterion via Join: $\top \leq a \sqcup b$

Informal description

Two elements $a$ and $b$ in a join-semilattice with a top element $\top$ are codisjoint if and only if the top element is less than or equal to their join, i.e., $\top \leq a \sqcup b$.

codisjoint_iff theorem

: Codisjoint a b ↔ a ⊔ b = ⊤

Full source

theorem codisjoint_iff : CodisjointCodisjoint a b ↔ a ⊔ b = ⊤ :=
  @disjoint_iff αᵒᵈ _ _ _ _

Codisjointness Criterion: $a \sqcup b = \top$

Informal description

Two elements $a$ and $b$ in a join-semilattice with a top element $\top$ are codisjoint if and only if their join equals $\top$, i.e., $a \sqcup b = \top$.

Codisjoint.top_le theorem

: Codisjoint a b → ⊤ ≤ a ⊔ b

Full source

theorem Codisjoint.top_le : Codisjoint a b → ⊤ ≤ a ⊔ b :=
  @Disjoint.le_bot αᵒᵈ _ _ _ _

Top Element is Below Join of Codisjoint Elements

Informal description

For any two codisjoint elements $a$ and $b$ in a join-semilattice with a top element $\top$, the top element is less than or equal to their join, i.e., $\top \leq a \sqcup b$.

codisjoint_assoc theorem

: Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)

Full source

theorem codisjoint_assoc : CodisjointCodisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c) :=
  @disjoint_assoc αᵒᵈ _ _ _ _ _

Associativity of Codisjointness in Join-Semilattices

Informal description

For elements $a, b, c$ in a join-semilattice with a top element $\top$, the elements $(a \sqcup b)$ and $c$ are codisjoint if and only if $a$ and $(b \sqcup c)$ are codisjoint. In other words, $$(a \sqcup b) \sqcup c = \top \Leftrightarrow a \sqcup (b \sqcup c) = \top.$$

codisjoint_left_comm theorem

: Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)

Full source

theorem codisjoint_left_comm : CodisjointCodisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c) :=
  @disjoint_left_comm αᵒᵈ _ _ _ _ _

Left Commutativity of Codisjointness in Join-Semilattices

Informal description

For elements $a, b, c$ in a join-semilattice with a top element $\top$, the element $a$ is codisjoint with $b \sqcup c$ if and only if $b$ is codisjoint with $a \sqcup c$. In other words, $$a \sqcup (b \sqcup c) = \top \Leftrightarrow b \sqcup (a \sqcup c) = \top.$$

codisjoint_right_comm theorem

: Codisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b

Full source

theorem codisjoint_right_comm : CodisjointCodisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b :=
  @disjoint_right_comm αᵒᵈ _ _ _ _ _

Right Commutativity of Codisjointness in Join-Semilattices

Informal description

For elements $a, b, c$ in a join-semilattice with a top element $\top$, the elements $(a \sqcup b)$ and $c$ are codisjoint if and only if the elements $(a \sqcup c)$ and $b$ are codisjoint. In other words, $$(a \sqcup b) \sqcup c = \top \Leftrightarrow (a \sqcup c) \sqcup b = \top.$$

Codisjoint.sup_left theorem

(h : Codisjoint a b) : Codisjoint (a ⊔ c) b

Full source

theorem Codisjoint.sup_left (h : Codisjoint a b) : Codisjoint (a ⊔ c) b :=
  h.mono_left le_sup_left

Codisjointness is preserved under left supremum

Informal description

Let $ a, b, c $ be elements of a lattice $ \alpha $ with a top element $ \top $. If $ a $ and $ b $ are codisjoint (i.e., $ a \sqcup b = \top $), then the supremum $ a \sqcup c $ and $ b $ are also codisjoint.

Codisjoint.sup_left' theorem

(h : Codisjoint a b) : Codisjoint (c ⊔ a) b

Full source

theorem Codisjoint.sup_left' (h : Codisjoint a b) : Codisjoint (c ⊔ a) b :=
  h.mono_left le_sup_right

Left Supremum Preserves Codisjointness

Informal description

Let $a$, $b$, and $c$ be elements of a lattice $\alpha$ with a top element $\top$. If $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then $c \sqcup a$ and $b$ are also codisjoint.

Codisjoint.sup_right theorem

(h : Codisjoint a b) : Codisjoint a (b ⊔ c)

Full source

theorem Codisjoint.sup_right (h : Codisjoint a b) : Codisjoint a (b ⊔ c) :=
  h.mono_right le_sup_left

Codisjointness is preserved under right supremum

Informal description

Let $a$, $b$, and $c$ be elements of a lattice $\alpha$ with a top element $\top$. If $a$ and $b$ are codisjoint (i.e., their join is $\top$), then $a$ and $b \sqcup c$ are also codisjoint.

Codisjoint.sup_right' theorem

(h : Codisjoint a b) : Codisjoint a (c ⊔ b)

Full source

theorem Codisjoint.sup_right' (h : Codisjoint a b) : Codisjoint a (c ⊔ b) :=
  h.mono_right le_sup_right

Codisjointness preserved under right supremum extension

Informal description

Let $a$, $b$, and $c$ be elements of a lattice $\alpha$ with a top element $\top$. If $a$ and $b$ are codisjoint (i.e., their join is $\top$), then $a$ and $c \sqcup b$ are also codisjoint.

Codisjoint.of_codisjoint_sup_of_le theorem

(h : Codisjoint (a ⊔ b) c) (hle : c ≤ a) : Codisjoint a b

Full source

theorem Codisjoint.of_codisjoint_sup_of_le (h : Codisjoint (a ⊔ b) c) (hle : c ≤ a) :
    Codisjoint a b :=
  @Disjoint.of_disjoint_inf_of_le αᵒᵈ _ _ _ _ _ h hle

Codisjointness from Join and Order Relation: $ (a \sqcup b) \perp c \land c \leq a \implies a \perp b $

Informal description

Let $ a $, $ b $, and $ c $ be elements of a lattice $ \alpha $ with a top element $ \top $. If the join $ a \sqcup b $ is codisjoint with $ c $ (i.e., $ (a \sqcup b) \sqcup c = \top $) and $ c \leq a $, then $ a $ and $ b $ are codisjoint (i.e., $ a \sqcup b = \top $).

Codisjoint.of_codisjoint_sup_of_le' theorem

(h : Codisjoint (a ⊔ b) c) (hle : c ≤ b) : Codisjoint a b

Full source

theorem Codisjoint.of_codisjoint_sup_of_le' (h : Codisjoint (a ⊔ b) c) (hle : c ≤ b) :
    Codisjoint a b :=
  @Disjoint.of_disjoint_inf_of_le' αᵒᵈ _ _ _ _ _ h hle

Codisjointness via Supremum and Order Condition: $ a \perp b $ via $(a \sqcup b) \perp c$ and $ c \leq b $

Informal description

Let $ a $, $ b $, and $ c $ be elements of a lattice with a top element $ \top $. If the supremum $ a \sqcup b $ is codisjoint with $ c $ (i.e., $(a \sqcup b) \sqcup c = \top$) and $ c \leq b $, then $ a $ and $ b $ are codisjoint (i.e., $ a \sqcup b = \top $).

codisjoint_inf_left theorem

: Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

Full source

@[simp]
theorem codisjoint_inf_left : CodisjointCodisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c := by
  simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]

Codisjointness Characterization via Meet: $(a \sqcap b) \perp c \leftrightarrow a \perp c \land b \perp c$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a top element $\top$, the meet $a \sqcap b$ is codisjoint with $c$ if and only if both $a$ and $b$ are individually codisjoint with $c$. In other words: $$ (a \sqcap b) \sqcup c = \top \leftrightarrow (a \sqcup c = \top) \land (b \sqcup c = \top). $$

codisjoint_inf_right theorem

: Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Full source

@[simp]
theorem codisjoint_inf_right : CodisjointCodisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c := by
  simp only [codisjoint_iff, sup_inf_left, inf_eq_top_iff]

Codisjointness Characterization via Meet: $a \perp (b \sqcap c) \leftrightarrow a \perp b \land a \perp c$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a top element $\top$, the element $a$ is codisjoint with the meet $b \sqcap c$ if and only if $a$ is codisjoint with both $b$ and $c$ individually. In other words: $$ a \sqcup (b \sqcap c) = \top \leftrightarrow (a \sqcup b = \top) \land (a \sqcup c = \top). $$

Codisjoint.inf_left theorem

(ha : Codisjoint a c) (hb : Codisjoint b c) : Codisjoint (a ⊓ b) c

Full source

theorem Codisjoint.inf_left (ha : Codisjoint a c) (hb : Codisjoint b c) : Codisjoint (a ⊓ b) c :=
  codisjoint_inf_left.2 ⟨ha, hb⟩

Codisjointness Preservation under Meet: $a \perp c \land b \perp c \to (a \sqcap b) \perp c$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a top element $\top$, if $a$ is codisjoint with $c$ and $b$ is codisjoint with $c$, then the meet $a \sqcap b$ is codisjoint with $c$. In other words: $$ \text{If } a \sqcup c = \top \text{ and } b \sqcup c = \top, \text{ then } (a \sqcap b) \sqcup c = \top. $$

Codisjoint.inf_right theorem

(hb : Codisjoint a b) (hc : Codisjoint a c) : Codisjoint a (b ⊓ c)

Full source

theorem Codisjoint.inf_right (hb : Codisjoint a b) (hc : Codisjoint a c) : Codisjoint a (b ⊓ c) :=
  codisjoint_inf_right.2 ⟨hb, hc⟩

Codisjointness Preservation under Meet: $a \perp b \land a \perp c \to a \perp (b \sqcap c)$

Informal description

For elements $a$, $b$, and $c$ in a lattice with a top element $\top$, if $a$ is codisjoint with $b$ and $a$ is codisjoint with $c$, then $a$ is codisjoint with the meet $b \sqcap c$. In other words: $$ \text{If } a \sqcup b = \top \text{ and } a \sqcup c = \top, \text{ then } a \sqcup (b \sqcap c) = \top. $$

Codisjoint.left_le_of_le_inf_right theorem

(h : a ⊓ b ≤ c) (hd : Codisjoint b c) : a ≤ c

Full source

theorem Codisjoint.left_le_of_le_inf_right (h : a ⊓ b ≤ c) (hd : Codisjoint b c) : a ≤ c :=
  @Disjoint.left_le_of_le_sup_right αᵒᵈ _ _ _ _ _ h hd.symm

Codisjointness Implication: $a \sqcap b \leq c$ and $b \sqcup c = \top$ implies $a \leq c$

Informal description

In a lattice $\alpha$ with a top element $\top$, if the meet $a \sqcap b$ is less than or equal to $c$ and $b$ is codisjoint with $c$ (i.e., $b \sqcup c = \top$), then $a$ is less than or equal to $c$.

Codisjoint.left_le_of_le_inf_left theorem

(h : b ⊓ a ≤ c) (hd : Codisjoint b c) : a ≤ c

Full source

theorem Codisjoint.left_le_of_le_inf_left (h : b ⊓ a ≤ c) (hd : Codisjoint b c) : a ≤ c :=
  hd.left_le_of_le_inf_right <| by rwa [inf_comm]

Codisjointness Implication: $b \sqcap a \leq c$ and $b \sqcup c = \top$ implies $a \leq c$

Informal description

In a lattice $\alpha$ with a top element $\top$, if the meet $b \sqcap a$ is less than or equal to $c$ and $b$ is codisjoint with $c$ (i.e., $b \sqcup c = \top$), then $a$ is less than or equal to $c$.

Disjoint.dual theorem

[PartialOrder α] [OrderBot α] {a b : α} : Disjoint a b → Codisjoint (toDual a) (toDual b)

Full source

theorem Disjoint.dual [PartialOrder α] [OrderBot α] {a b : α} :
    Disjoint a b → Codisjoint (toDual a) (toDual b) :=
  id

Dual of Disjoint Elements is Codisjoint in Order Dual

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot$. For any two elements $a, b \in \alpha$ that are disjoint (i.e., their infimum is $\bot$), their order duals $\text{toDual}(a)$ and $\text{toDual}(b)$ in the order dual $\alpha^{\text{op}}$ are codisjoint (i.e., their supremum is $\top$).

Codisjoint.dual theorem

[PartialOrder α] [OrderTop α] {a b : α} : Codisjoint a b → Disjoint (toDual a) (toDual b)

Full source

theorem Codisjoint.dual [PartialOrder α] [OrderTop α] {a b : α} :
    Codisjoint a b → Disjoint (toDual a) (toDual b) :=
  id

Duality between Codisjoint and Disjoint Elements via Order Dual

Informal description

Let $\alpha$ be a partially ordered set with a greatest element $\top$. For any elements $a, b \in \alpha$, if $a$ and $b$ are codisjoint (i.e., their join is $\top$), then their images under the order duality operation are disjoint (i.e., their meet is $\bot$ in the dual order).

disjoint_toDual_iff theorem

[PartialOrder α] [OrderTop α] {a b : α} : Disjoint (toDual a) (toDual b) ↔ Codisjoint a b

Full source

@[simp]
theorem disjoint_toDual_iff [PartialOrder α] [OrderTop α] {a b : α} :
    DisjointDisjoint (toDual a) (toDual b) ↔ Codisjoint a b :=
  Iff.rfl

Disjointness in Order Dual Equivalent to Codisjointness in Original Lattice

Informal description

Let $\alpha$ be a partially ordered set with a greatest element $\top$. For any elements $a, b \in \alpha$, the elements $\text{toDual}(a)$ and $\text{toDual}(b)$ in the order dual $\alpha^{\text{op}}$ are disjoint if and only if $a$ and $b$ are codisjoint in $\alpha$. Here, $\text{toDual}(x)$ denotes the element $x$ viewed in the order dual lattice $\alpha^{\text{op}}$, where the order is reversed.

disjoint_ofDual_iff theorem

[PartialOrder α] [OrderBot α] {a b : αᵒᵈ} : Disjoint (ofDual a) (ofDual b) ↔ Codisjoint a b

Full source

@[simp]
theorem disjoint_ofDual_iff [PartialOrder α] [OrderBot α] {a b : αᵒᵈ} :
    DisjointDisjoint (ofDual a) (ofDual b) ↔ Codisjoint a b :=
  Iff.rfl

Disjointness in Order Dual via Codisjointness: $\text{Disjoint}(\text{ofDual}(a), \text{ofDual}(b)) \leftrightarrow \text{Codisjoint}(a, b)$

Informal description

Let $\alpha$ be a partially ordered set with a bottom element $\bot$, and let $a, b$ be elements of the order dual $\alpha^{\text{op}}$. Then the elements $\text{ofDual}(a)$ and $\text{ofDual}(b)$ are disjoint in $\alpha$ (i.e., their infimum is $\bot$) if and only if $a$ and $b$ are codisjoint in $\alpha^{\text{op}}$ (i.e., their supremum is $\top$).

codisjoint_toDual_iff theorem

[PartialOrder α] [OrderBot α] {a b : α} : Codisjoint (toDual a) (toDual b) ↔ Disjoint a b

Full source

@[simp]
theorem codisjoint_toDual_iff [PartialOrder α] [OrderBot α] {a b : α} :
    CodisjointCodisjoint (toDual a) (toDual b) ↔ Disjoint a b :=
  Iff.rfl

Codisjointness in Order Dual is Equivalent to Disjointness in Original Order

Informal description

Let $\alpha$ be a partially ordered set with a bottom element $\bot$. For any elements $a, b \in \alpha$, the elements $\text{toDual}(a)$ and $\text{toDual}(b)$ in the order dual $\alpha^{\text{op}}$ are codisjoint if and only if $a$ and $b$ are disjoint in $\alpha$. Here, two elements $x, y$ are *disjoint* if their infimum is $\bot$, and two elements $u, v$ are *codisjoint* if their supremum is $\top$ (the top element in the lattice).

codisjoint_ofDual_iff theorem

[PartialOrder α] [OrderTop α] {a b : αᵒᵈ} : Codisjoint (ofDual a) (ofDual b) ↔ Disjoint a b

Full source

@[simp]
theorem codisjoint_ofDual_iff [PartialOrder α] [OrderTop α] {a b : αᵒᵈ} :
    CodisjointCodisjoint (ofDual a) (ofDual b) ↔ Disjoint a b :=
  Iff.rfl

Codisjointness under Order Dual ↔ Disjointness in Dual Order

Informal description

Let $\alpha$ be a partially ordered set with a greatest element $\top$, and let $a, b$ be elements of the order dual $\alpha^{\text{op}}$. Then the elements $\text{ofDual}(a)$ and $\text{ofDual}(b)$ are codisjoint in $\alpha$ if and only if $a$ and $b$ are disjoint in $\alpha^{\text{op}}$.

Disjoint.le_of_codisjoint theorem

(hab : Disjoint a b) (hbc : Codisjoint b c) : a ≤ c

Full source

theorem Disjoint.le_of_codisjoint (hab : Disjoint a b) (hbc : Codisjoint b c) : a ≤ c := by
  rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
  exact inf_le_inf_right _ le_sup_left

Disjoint and Codisjoint Elements Imply Order Relation: $a \sqcap b = \bot \land b \sqcup c = \top \Rightarrow a \leq c$

Informal description

In a bounded lattice $\alpha$, if elements $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$) and $b$ and $c$ are codisjoint (i.e., $b \sqcup c = \top$), then $a \leq c$.

IsCompl structure

[PartialOrder α] [BoundedOrder α] (x y : α)

Full source

/-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`. -/
structure IsCompl [PartialOrder α] [BoundedOrder α] (x y : α) : Prop where
  /-- If `x` and `y` are to be complementary in an order, they should be disjoint. -/
  protected disjoint : Disjoint x y
  /-- If `x` and `y` are to be complementary in an order, they should be codisjoint. -/
  protected codisjoint : Codisjoint x y

Complementary elements in a bounded lattice

Informal description

In a bounded lattice $\alpha$, two elements $x$ and $y$ are complements of each other if their join is the top element ($x \sqcup y = \top$) and their meet is the bottom element ($x \sqcap y = \bot$).

isCompl_iff theorem

[PartialOrder α] [BoundedOrder α] {a b : α} : IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b

Full source

theorem isCompl_iff [PartialOrder α] [BoundedOrder α] {a b : α} :
    IsComplIsCompl a b ↔ Disjoint a b ∧ Codisjoint a b :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Characterization of Complementary Elements in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, two elements $a$ and $b$ are complements of each other if and only if they are disjoint (i.e., $a \sqcap b = \bot$) and codisjoint (i.e., $a \sqcup b = \top$).

IsCompl.symm theorem

(h : IsCompl x y) : IsCompl y x

Full source

@[symm]
protected theorem symm (h : IsCompl x y) : IsCompl y x :=
  ⟨h.1.symm, h.2.symm⟩

Symmetry of Complementarity in a Bounded Lattice

Informal description

In a bounded lattice, if $x$ and $y$ are complements of each other (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$), then $y$ and $x$ are also complements of each other.

isCompl_comm theorem

: IsCompl x y ↔ IsCompl y x

Full source

lemma _root_.isCompl_comm : IsComplIsCompl x y ↔ IsCompl y x := ⟨IsCompl.symm, IsCompl.symm⟩

Symmetry of Complementarity in a Bounded Lattice

Informal description

In a bounded lattice, two elements $x$ and $y$ are complements of each other if and only if $y$ and $x$ are complements of each other. That is, $x \sqcap y = \bot$ and $x \sqcup y = \top$ holds if and only if $y \sqcap x = \bot$ and $y \sqcup x = \top$ holds.

IsCompl.dual theorem

(h : IsCompl x y) : IsCompl (toDual x) (toDual y)

Full source

theorem dual (h : IsCompl x y) : IsCompl (toDual x) (toDual y) :=
  ⟨h.2, h.1⟩

Complementarity Preserved Under Order Duality

Informal description

In a bounded lattice $\alpha$, if two elements $x$ and $y$ are complements of each other (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$), then their order duals $\text{toDual}(x)$ and $\text{toDual}(y)$ are also complements of each other in the order dual lattice $\alpha^{\text{op}}$.

IsCompl.ofDual theorem

{a b : αᵒᵈ} (h : IsCompl a b) : IsCompl (ofDual a) (ofDual b)

Full source

theorem ofDual {a b : αᵒᵈ} (h : IsCompl a b) : IsCompl (ofDual a) (ofDual b) :=
  ⟨h.2, h.1⟩

Complement Preservation under Order Dual Isomorphism

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$ of a bounded lattice $\alpha$, if $a$ and $b$ are complements in $\alpha^{\text{op}}$, then their images under the order dual isomorphism $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ are complements in $\alpha$. That is, if $a \sqcap b = \bot$ and $a \sqcup b = \top$ in $\alpha^{\text{op}}$, then $\text{ofDual}(a) \sqcap \text{ofDual}(b) = \bot$ and $\text{ofDual}(a) \sqcup \text{ofDual}(b) = \top$ in $\alpha$.

IsCompl.of_le theorem

(h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y

Full source

theorem of_le (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y :=
  ⟨disjoint_iff_inf_le.mpr h₁, codisjoint_iff_le_sup.mpr h₂⟩

Complement Criterion via Meet and Join Inequalities

Informal description

In a bounded lattice $\alpha$, two elements $x$ and $y$ are complements of each other if their meet is less than or equal to the bottom element ($x \sqcap y \leq \bot$) and their join is greater than or equal to the top element ($\top \leq x \sqcup y$).

IsCompl.of_eq theorem

(h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : IsCompl x y

Full source

theorem of_eq (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : IsCompl x y :=
  ⟨disjoint_iff.mpr h₁, codisjoint_iff.mpr h₂⟩

Complement Criterion via Meet and Join Equalities

Informal description

In a bounded lattice $\alpha$, two elements $x$ and $y$ are complements of each other if their meet is the bottom element ($x \sqcap y = \bot$) and their join is the top element ($x \sqcup y = \top$).

IsCompl.inf_eq_bot theorem

(h : IsCompl x y) : x ⊓ y = ⊥

Full source

theorem inf_eq_bot (h : IsCompl x y) : x ⊓ y = ⊥ :=
  h.disjoint.eq_bot

Meet of complementary elements equals bottom

Informal description

For any two elements $x$ and $y$ in a bounded lattice $\alpha$, if $x$ and $y$ are complements (i.e., $x \sqcup y = \top$ and $x \sqcap y = \bot$), then their meet is the bottom element: $x \sqcap y = \bot$.

IsCompl.sup_eq_top theorem

(h : IsCompl x y) : x ⊔ y = ⊤

Full source

theorem sup_eq_top (h : IsCompl x y) : x ⊔ y = ⊤ :=
  h.codisjoint.eq_top

Join of complementary elements equals top

Informal description

For any two elements $x$ and $y$ in a bounded lattice, if $x$ and $y$ are complements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$), then their join is the top element: $x \sqcup y = \top$.

IsCompl.inf_left_le_of_le_sup_right theorem

(h : IsCompl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b

Full source

theorem inf_left_le_of_le_sup_right (h : IsCompl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b :=
  calc
    a ⊓ x ≤ (b ⊔ y) ⊓ x := inf_le_inf hle le_rfl
    _ = b ⊓ xb ⊓ x ⊔ y ⊓ x := inf_sup_right _ _ _
    _ = b ⊓ x := by rw [h.symm.inf_eq_bot, sup_bot_eq]
    _ ≤ b := inf_le_left

Complementary Elements Imply Infimum Inequality: $a \leq b \sqcup y \Rightarrow a \sqcap x \leq b$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any elements $a, b \in \alpha$, if $a \leq b \sqcup y$, then $a \sqcap x \leq b$.

IsCompl.le_sup_right_iff_inf_left_le theorem

{a b} (h : IsCompl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b

Full source

theorem le_sup_right_iff_inf_left_le {a b} (h : IsCompl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b :=
  ⟨h.inf_left_le_of_le_sup_right, h.symm.dual.inf_left_le_of_le_sup_right⟩

Complementary Elements Induce Galois Connection: $a \leq b \sqcup y \leftrightarrow a \sqcap x \leq b$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any elements $a, b \in \alpha$, the following equivalence holds: $$a \leq b \sqcup y \quad \text{if and only if} \quad a \sqcap x \leq b.$$

IsCompl.inf_left_eq_bot_iff theorem

(h : IsCompl y z) : x ⊓ y = ⊥ ↔ x ≤ z

Full source

theorem inf_left_eq_bot_iff (h : IsCompl y z) : x ⊓ yx ⊓ y = ⊥ ↔ x ≤ z := by
  rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

Complementary Elements Characterization: $x \sqcap y = \bot \leftrightarrow x \leq z$

Informal description

Let $\alpha$ be a bounded lattice, and let $y, z \in \alpha$ be complementary elements (i.e., $y \sqcap z = \bot$ and $y \sqcup z = \top$). For any element $x \in \alpha$, the meet of $x$ and $y$ is the bottom element if and only if $x$ is less than or equal to $z$, i.e., $$x \sqcap y = \bot \leftrightarrow x \leq z.$$

IsCompl.inf_right_eq_bot_iff theorem

(h : IsCompl y z) : x ⊓ z = ⊥ ↔ x ≤ y

Full source

theorem inf_right_eq_bot_iff (h : IsCompl y z) : x ⊓ zx ⊓ z = ⊥ ↔ x ≤ y :=
  h.symm.inf_left_eq_bot_iff

Complementary Elements Characterization: $x \sqcap z = \bot \leftrightarrow x \leq y$

Informal description

Let $\alpha$ be a bounded lattice, and let $y, z \in \alpha$ be complementary elements (i.e., $y \sqcap z = \bot$ and $y \sqcup z = \top$). For any element $x \in \alpha$, the meet of $x$ and $z$ is the bottom element if and only if $x$ is less than or equal to $y$, i.e., $$x \sqcap z = \bot \leftrightarrow x \leq y.$$

IsCompl.disjoint_left_iff theorem

(h : IsCompl y z) : Disjoint x y ↔ x ≤ z

Full source

theorem disjoint_left_iff (h : IsCompl y z) : DisjointDisjoint x y ↔ x ≤ z := by
  rw [disjoint_iff]
  exact h.inf_left_eq_bot_iff

Disjointness Criterion for Complementary Elements: $x \sqcap y = \bot \leftrightarrow x \leq z$

Informal description

Let $\alpha$ be a bounded lattice, and let $y, z \in \alpha$ be complementary elements (i.e., $y \sqcap z = \bot$ and $y \sqcup z = \top$). For any element $x \in \alpha$, the elements $x$ and $y$ are disjoint if and only if $x$ is less than or equal to $z$, i.e., $$x \sqcap y = \bot \leftrightarrow x \leq z.$$

IsCompl.disjoint_right_iff theorem

(h : IsCompl y z) : Disjoint x z ↔ x ≤ y

Full source

theorem disjoint_right_iff (h : IsCompl y z) : DisjointDisjoint x z ↔ x ≤ y :=
  h.symm.disjoint_left_iff

Disjointness Criterion for Complementary Elements: $x \sqcap z = \bot \leftrightarrow x \leq y$

Informal description

Let $\alpha$ be a bounded lattice, and let $y, z \in \alpha$ be complementary elements (i.e., $y \sqcap z = \bot$ and $y \sqcup z = \top$). For any element $x \in \alpha$, the elements $x$ and $z$ are disjoint if and only if $x$ is less than or equal to $y$, i.e., $$x \sqcap z = \bot \leftrightarrow x \leq y.$$

IsCompl.le_left_iff theorem

(h : IsCompl x y) : z ≤ x ↔ Disjoint z y

Full source

theorem le_left_iff (h : IsCompl x y) : z ≤ x ↔ Disjoint z y :=
  h.disjoint_right_iff.symm

Order-Disjointness Criterion for Complementary Elements: $z \leq x \leftrightarrow z \sqcap y = \bot$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any element $z \in \alpha$, the inequality $z \leq x$ holds if and only if $z$ and $y$ are disjoint, i.e., $$z \leq x \leftrightarrow z \sqcap y = \bot.$$

IsCompl.le_right_iff theorem

(h : IsCompl x y) : z ≤ y ↔ Disjoint z x

Full source

theorem le_right_iff (h : IsCompl x y) : z ≤ y ↔ Disjoint z x :=
  h.symm.le_left_iff

Order-Disjointness Criterion for Complementary Elements: $z \leq y \leftrightarrow z \sqcap x = \bot$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any element $z \in \alpha$, the inequality $z \leq y$ holds if and only if $z$ and $x$ are disjoint, i.e., $$z \leq y \leftrightarrow z \sqcap x = \bot.$$

IsCompl.left_le_iff theorem

(h : IsCompl x y) : x ≤ z ↔ Codisjoint z y

Full source

theorem left_le_iff (h : IsCompl x y) : x ≤ z ↔ Codisjoint z y :=
  h.dual.le_left_iff

Order-Codisjointness Criterion for Complementary Elements: $x \leq z \leftrightarrow z \sqcup y = \top$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any element $z \in \alpha$, the inequality $x \leq z$ holds if and only if $z$ and $y$ are codisjoint, i.e., $$x \leq z \leftrightarrow z \sqcup y = \top.$$

IsCompl.right_le_iff theorem

(h : IsCompl x y) : y ≤ z ↔ Codisjoint z x

Full source

theorem right_le_iff (h : IsCompl x y) : y ≤ z ↔ Codisjoint z x :=
  h.symm.left_le_iff

Order-Codisjointness Criterion for Complementary Elements: $y \leq z \leftrightarrow z \sqcup x = \top$

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y \in \alpha$ be complementary elements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). For any element $z \in \alpha$, the inequality $y \leq z$ holds if and only if $z$ and $x$ are codisjoint, i.e., $$y \leq z \leftrightarrow z \sqcup x = \top.$$

IsCompl.Antitone theorem

{x' y'} (h : IsCompl x y) (h' : IsCompl x' y') (hx : x ≤ x') : y' ≤ y

Full source

protected theorem Antitone {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') (hx : x ≤ x') : y' ≤ y :=
  h'.right_le_iff.2 <| h.symm.codisjoint.mono_right hx

Antitone Property of Complements in a Bounded Lattice

Informal description

Let $\alpha$ be a bounded lattice, and let $x, y, x', y' \in \alpha$ be elements such that $x$ and $y$ are complements (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$) and $x'$ and $y'$ are complements. If $x \leq x'$, then $y' \leq y$.

IsCompl.right_unique theorem

(hxy : IsCompl x y) (hxz : IsCompl x z) : y = z

Full source

theorem right_unique (hxy : IsCompl x y) (hxz : IsCompl x z) : y = z :=
  le_antisymm (hxz.Antitone hxy <| le_refl x) (hxy.Antitone hxz <| le_refl x)

Uniqueness of Complements in a Bounded Lattice

Informal description

In a bounded lattice, if an element $x$ has two complements $y$ and $z$ (i.e., $x \sqcap y = \bot$, $x \sqcup y = \top$, $x \sqcap z = \bot$, and $x \sqcup z = \top$), then $y = z$.

IsCompl.left_unique theorem

(hxz : IsCompl x z) (hyz : IsCompl y z) : x = y

Full source

theorem left_unique (hxz : IsCompl x z) (hyz : IsCompl y z) : x = y :=
  hxz.symm.right_unique hyz.symm

Uniqueness of Left Complements in a Bounded Lattice

Informal description

In a bounded lattice, if two elements $x$ and $y$ both have the same complement $z$ (i.e., $x \sqcap z = \bot$, $x \sqcup z = \top$, $y \sqcap z = \bot$, and $y \sqcup z = \top$), then $x = y$.

IsCompl.sup_inf theorem

{x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊔ x') (y ⊓ y')

Full source

theorem sup_inf {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊔ x') (y ⊓ y') :=
  of_eq
    (by rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
      h'.inf_eq_bot, inf_bot_eq])
    (by rw [sup_inf_left, sup_comm x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq,
      sup_assoc, sup_left_comm, h'.sup_eq_top, sup_top_eq])

Complementarity Preservation under Supremum and Infimum: $(x \sqcup x', y \sqcap y')$ is complementary when $(x, y)$ and $(x', y')$ are

Informal description

Let $\alpha$ be a bounded lattice. Given two pairs of complementary elements $(x, y)$ and $(x', y')$ in $\alpha$ (i.e., $x \sqcap y = \bot$, $x \sqcup y = \top$, $x' \sqcap y' = \bot$, and $x' \sqcup y' = \top$), then the pair $(x \sqcup x', y \sqcap y')$ is also complementary, i.e., $(x \sqcup x') \sqcap (y \sqcap y') = \bot$ and $(x \sqcup x') \sqcup (y \sqcap y') = \top$.

IsCompl.inf_sup theorem

{x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊓ x') (y ⊔ y')

Full source

theorem inf_sup {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊓ x') (y ⊔ y') :=
  (h.symm.sup_inf h'.symm).symm

Complementarity Preservation under Infimum and Supremum: $(x \sqcap x', y \sqcup y')$ is complementary when $(x, y)$ and $(x', y')$ are

Informal description

Let $\alpha$ be a bounded lattice. Given two pairs of complementary elements $(x, y)$ and $(x', y')$ in $\alpha$ (i.e., $x \sqcap y = \bot$, $x \sqcup y = \top$, $x' \sqcap y' = \bot$, and $x' \sqcup y' = \top$), then the pair $(x \sqcap x', y \sqcup y')$ is also complementary, i.e., $(x \sqcap x') \sqcap (y \sqcup y') = \bot$ and $(x \sqcap x') \sqcup (y \sqcup y') = \top$.

Prod.disjoint_iff theorem

[OrderBot α] [OrderBot β] {x y : α × β} : Disjoint x y ↔ Disjoint x.1 y.1 ∧ Disjoint x.2 y.2

Full source

protected theorem disjoint_iff [OrderBot α] [OrderBot β] {x y : α × β} :
    DisjointDisjoint x y ↔ Disjoint x.1 y.1 ∧ Disjoint x.2 y.2 := by
  constructor
  · intro h
    refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
    all_goals exact bot_le
  · rintro ⟨ha, hb⟩ z hza hzb
    exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

Disjointness in Product Lattices: $x \sqcap y = \bot$ iff componentwise disjointness

Informal description

Let $\alpha$ and $\beta$ be lattices with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product lattice $\alpha \times \beta$, the elements $x$ and $y$ are disjoint (i.e., $x \sqcap y = (\bot_\alpha, \bot_\beta)$) if and only if $x_1$ and $y_1$ are disjoint in $\alpha$ and $x_2$ and $y_2$ are disjoint in $\beta$.

Prod.codisjoint_iff theorem

[OrderTop α] [OrderTop β] {x y : α × β} : Codisjoint x y ↔ Codisjoint x.1 y.1 ∧ Codisjoint x.2 y.2

Full source

protected theorem codisjoint_iff [OrderTop α] [OrderTop β] {x y : α × β} :
    CodisjointCodisjoint x y ↔ Codisjoint x.1 y.1 ∧ Codisjoint x.2 y.2 :=
  @Prod.disjoint_iff αᵒᵈ βᵒᵈ _ _ _ _ _ _

Codisjointness in Product Lattices: $x \sqcup y = \top$ iff componentwise codisjointness

Informal description

Let $\alpha$ and $\beta$ be lattices with top elements $\top_\alpha$ and $\top_\beta$ respectively. For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product lattice $\alpha \times \beta$, the elements $x$ and $y$ are codisjoint (i.e., $x \sqcup y = (\top_\alpha, \top_\beta)$) if and only if $x_1$ and $y_1$ are codisjoint in $\alpha$ and $x_2$ and $y_2$ are codisjoint in $\beta$.

Prod.isCompl_iff theorem

[BoundedOrder α] [BoundedOrder β] {x y : α × β} : IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2

Full source

protected theorem isCompl_iff [BoundedOrder α] [BoundedOrder β] {x y : α × β} :
    IsComplIsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2 := by
  simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]

Complement Decomposition in Product Lattices

Informal description

Let $\alpha$ and $\beta$ be bounded lattices, and let $x = (x_1, x_2)$ and $y = (y_1, y_2)$ be elements of the product lattice $\alpha \times \beta$. Then $x$ and $y$ are complements in $\alpha \times \beta$ if and only if $x_1$ and $y_1$ are complements in $\alpha$, and $x_2$ and $y_2$ are complements in $\beta$. In other words, $x \sqcup y = (\top, \top)$ and $x \sqcap y = (\bot, \bot)$ if and only if $x_1 \sqcup y_1 = \top$, $x_1 \sqcap y_1 = \bot$, $x_2 \sqcup y_2 = \top$, and $x_2 \sqcap y_2 = \bot$.

isCompl_toDual_iff theorem

: IsCompl (toDual a) (toDual b) ↔ IsCompl a b

Full source

@[simp]
theorem isCompl_toDual_iff : IsComplIsCompl (toDual a) (toDual b) ↔ IsCompl a b :=
  ⟨IsCompl.ofDual, IsCompl.dual⟩

Complementarity in Order Dual Lattice $\alpha^{\text{op}}$ iff Complementarity in $\alpha$

Informal description

For any elements $a$ and $b$ in a bounded lattice $\alpha$, the order duals $\text{toDual}(a)$ and $\text{toDual}(b)$ are complements in the order dual lattice $\alpha^{\text{op}}$ if and only if $a$ and $b$ are complements in $\alpha$. In other words, $\text{toDual}(a) \sqcap \text{toDual}(b) = \bot$ and $\text{toDual}(a) \sqcup \text{toDual}(b) = \top$ in $\alpha^{\text{op}}$ if and only if $a \sqcap b = \bot$ and $a \sqcup b = \top$ in $\alpha$.

isCompl_ofDual_iff theorem

{a b : αᵒᵈ} : IsCompl (ofDual a) (ofDual b) ↔ IsCompl a b

Full source

@[simp]
theorem isCompl_ofDual_iff {a b : αᵒᵈ} : IsComplIsCompl (ofDual a) (ofDual b) ↔ IsCompl a b :=
  ⟨IsCompl.dual, IsCompl.ofDual⟩

Complement Preservation under Order Dual Isomorphism (iff version)

Informal description

For any elements $a$ and $b$ in the order dual lattice $\alpha^{\text{op}}$, the images $\text{ofDual}(a)$ and $\text{ofDual}(b)$ are complements in $\alpha$ if and only if $a$ and $b$ are complements in $\alpha^{\text{op}}$. That is, $\text{ofDual}(a) \sqcap \text{ofDual}(b) = \bot$ and $\text{ofDual}(a) \sqcup \text{ofDual}(b) = \top$ in $\alpha$ if and only if $a \sqcap b = \bot$ and $a \sqcup b = \top$ in $\alpha^{\text{op}}$.

isCompl_bot_top theorem

: IsCompl (⊥ : α) ⊤

Full source

theorem isCompl_bot_top : IsCompl (⊥ : α) ⊤ :=
  IsCompl.of_eq (bot_inf_eq _) (sup_top_eq _)

Bottom and Top are Complements in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, the bottom element $\bot$ and the top element $\top$ are complements of each other, i.e., $\bot \sqcap \top = \bot$ and $\bot \sqcup \top = \top$.

isCompl_top_bot theorem

: IsCompl (⊤ : α) ⊥

Full source

theorem isCompl_top_bot : IsCompl (⊤ : α) ⊥ :=
  IsCompl.of_eq (inf_bot_eq _) (top_sup_eq _)

Top and Bottom Elements are Complements in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, the top element $\top$ and the bottom element $\bot$ are complements of each other, i.e., $\top \sqcap \bot = \bot$ and $\top \sqcup \bot = \top$.

IsComplemented definition

(a : α) : Prop

Full source

/-- An element is *complemented* if it has a complement. -/
def IsComplemented (a : α) : Prop :=
  ∃ b, IsCompl a b

Complemented element in a bounded lattice

Informal description

An element $a$ in a bounded lattice $\alpha$ is called *complemented* if there exists an element $b$ such that $a$ and $b$ are complements of each other, i.e., their join is the top element ($a \sqcup b = \top$) and their meet is the bottom element ($a \sqcap b = \bot$).

isComplemented_bot theorem

: IsComplemented (⊥ : α)

Full source

theorem isComplemented_bot : IsComplemented (⊥ : α) :=
  ⟨⊤, isCompl_bot_top⟩

Bottom Element is Complemented in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, the bottom element $\bot$ is complemented, meaning there exists an element $x$ such that $\bot \sqcap x = \bot$ and $\bot \sqcup x = \top$.

isComplemented_top theorem

: IsComplemented (⊤ : α)

Full source

theorem isComplemented_top : IsComplemented (⊤ : α) :=
  ⟨⊥, isCompl_top_bot⟩

Top Element is Complemented in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, the top element $\top$ is complemented, meaning there exists an element $x$ such that $\top \sqcap x = \bot$ and $\top \sqcup x = \top$.

IsComplemented.sup theorem

: IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b)

Full source

theorem IsComplemented.sup : IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b) :=
  fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊓ b', ha.sup_inf hb⟩

Supremum of Complemented Elements is Complemented

Informal description

In a bounded lattice $\alpha$, if elements $a$ and $b$ are complemented (i.e., have complements), then their supremum $a \sqcup b$ is also complemented.

IsComplemented.inf theorem

: IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b)

Full source

theorem IsComplemented.inf : IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b) :=
  fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊔ b', ha.inf_sup hb⟩

Infimum of Complemented Elements is Complemented in a Bounded Lattice

Informal description

In a bounded lattice $\alpha$, if elements $a$ and $b$ are complemented (i.e., there exist elements $a'$ and $b'$ such that $a \sqcap a' = \bot$, $a \sqcup a' = \top$, $b \sqcap b' = \bot$, and $b \sqcup b' = \top$), then their infimum $a \sqcap b$ is also complemented.

ComplementedLattice structure

(α) [Lattice α] [BoundedOrder α]

Full source

/-- A complemented bounded lattice is one where every element has a (not necessarily unique)
complement. -/
class ComplementedLattice (α) [Lattice α] [BoundedOrder α] : Prop where
  /-- In a `ComplementedLattice`, every element admits a complement. -/
  exists_isCompl : ∀ a : α, ∃ b : α, IsCompl a b

Complemented Lattice

Informal description

A complemented lattice is a bounded lattice where every element has a (not necessarily unique) complement. That is, for every element $a$ in the lattice, there exists an element $b$ such that the infimum of $a$ and $b$ is the bottom element $\bot$ and the supremum of $a$ and $b$ is the top element $\top$.

complementedLattice_iff theorem

(α) [Lattice α] [BoundedOrder α] : ComplementedLattice α ↔ ∀ a : α, ∃ b : α, IsCompl a b

Full source

lemma complementedLattice_iff (α) [Lattice α] [BoundedOrder α] :
    ComplementedLatticeComplementedLattice α ↔ ∀ a : α, ∃ b : α, IsCompl a b :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Characterization of Complemented Lattices via Existence of Complements

Informal description

A bounded lattice $\alpha$ is complemented if and only if for every element $a \in \alpha$, there exists an element $b \in \alpha$ such that $a$ and $b$ are complements, i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$.

Subsingleton.instComplementedLattice instance

[Lattice α] [BoundedOrder α] [Subsingleton α] : ComplementedLattice α

Full source

instance Subsingleton.instComplementedLattice
    [Lattice α] [BoundedOrder α] [Subsingleton α] : ComplementedLattice α := by
  refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
  rw [Subsingleton.elim ⊥ ⊤]
  exact codisjoint_top_right

Complemented Lattice Structure on Subsingleton Lattices

Informal description

Every subsingleton lattice with a bounded order is a complemented lattice.

ComplementedLattice.instOrderDual instance

: ComplementedLattice αᵒᵈ

Full source

instance : ComplementedLattice αᵒᵈ :=
  ⟨fun a ↦
    let ⟨b, hb⟩ := exists_isCompl (show α from a)
    ⟨b, hb.dual⟩⟩

Complemented Lattice Duality

Informal description

The order dual of a complemented lattice is also a complemented lattice. That is, if $\alpha$ is a complemented lattice, then $\alpha^{\text{op}}$ is also a complemented lattice.

Complementeds abbrev

(α : Type*) [Lattice α] [BoundedOrder α] : Type _

Full source

/-- The sublattice of complemented elements. -/
abbrev Complementeds (α : Type*) [Lattice α] [BoundedOrder α] : Type _ :=
  {a : α // IsComplemented a}

Sublattice of Complemented Elements in a Bounded Lattice

Informal description

Given a bounded lattice $\alpha$ (i.e., a lattice with both a top element $\top$ and a bottom element $\bot$), the type `Complementeds α` represents the sublattice consisting of all complemented elements of $\alpha$. An element $a \in \alpha$ is *complemented* if there exists an element $b \in \alpha$ such that $a \sqcup b = \top$ and $a \sqcap b = \bot$.

Complementeds.hasCoeT instance

: CoeTC (Complementeds α) α

Full source

instance hasCoeT : CoeTC (Complementeds α) α := ⟨Subtype.val⟩

Canonical Embedding of Complemented Elements into a Bounded Lattice

Informal description

The type `Complementeds α` of complemented elements in a bounded lattice $\alpha$ can be canonically embedded into $\alpha$ via the inclusion map.

Complementeds.coe_injective theorem

: Injective ((↑) : Complementeds α → α)

Full source

theorem coe_injective : Injective ((↑) : Complementeds α → α) := Subtype.coe_injective

Injectivity of the Complemented Elements Embedding

Informal description

The canonical embedding from the type `Complementeds α` (consisting of complemented elements in a bounded lattice `α`) to `α` is injective. That is, for any two elements `a, b` in `Complementeds α`, if their images in `α` are equal (`(a : α) = (b : α)`), then `a = b` in `Complementeds α`.

Complementeds.coe_inj theorem

: (a : α) = b ↔ a = b

Full source

@[simp, norm_cast]
theorem coe_inj : (a : α) = b ↔ a = b := Subtype.coe_inj

Equality in Sublattice of Complemented Elements via Parent Lattice Equality

Informal description

For any two elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the equality $a = b$ holds in $\alpha$ if and only if $a = b$ holds in the sublattice.

Complementeds.coe_le_coe theorem

: (a : α) ≤ b ↔ a ≤ b

Full source

@[norm_cast]
theorem coe_le_coe : (a : α) ≤ b ↔ a ≤ b := by simp

Order Preservation in Sublattice of Complemented Elements

Informal description

For any two elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the inequality $a \leq b$ holds in $\alpha$ if and only if $a \leq b$ holds in the sublattice of complemented elements.

Complementeds.coe_lt_coe theorem

: (a : α) < b ↔ a < b

Full source

@[norm_cast]
theorem coe_lt_coe : (a : α) < b ↔ a < b := by simp

Order Preservation in Sublattice of Complemented Elements

Informal description

For any two elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the inequality $a < b$ holds in the sublattice if and only if it holds in the original lattice $\alpha$.

Complementeds.instBoundedOrder instance

: BoundedOrder (Complementeds α)

Full source

instance : BoundedOrder (Complementeds α) :=
  Subtype.boundedOrder isComplemented_bot isComplemented_top

Bounded Order Structure on Complemented Elements

Informal description

The sublattice of complemented elements in a bounded lattice $\alpha$ is itself a bounded order, with the same top and bottom elements as $\alpha$.

Complementeds.coe_bot theorem

: ((⊥ : Complementeds α) : α) = ⊥

Full source

@[simp, norm_cast]
theorem coe_bot : ((⊥ : Complementeds α) : α) = ⊥ := rfl

Bottom Element Preservation in Sublattice of Complemented Elements

Informal description

The bottom element of the sublattice of complemented elements in a bounded lattice $\alpha$ is equal to the bottom element of $\alpha$ itself, i.e., $\bot_{\text{Complementeds }\alpha} = \bot_\alpha$.

Complementeds.coe_top theorem

: ((⊤ : Complementeds α) : α) = ⊤

Full source

@[simp, norm_cast]
theorem coe_top : ((⊤ : Complementeds α) : α) = ⊤ := rfl

Top Element of Complemented Sublattice Equals Top Element of Lattice

Informal description

In a bounded lattice $\alpha$, the top element of the sublattice of complemented elements, when viewed as an element of $\alpha$, is equal to the top element of $\alpha$.

Complementeds.mk_bot theorem

: (⟨⊥, isComplemented_bot⟩ : Complementeds α) = ⊥

Full source

theorem mk_bot : (⟨⊥, isComplemented_bot⟩ : Complementeds α) = ⊥ := by simp

Bottom Element Construction in Complemented Sublattice

Informal description

In a bounded lattice $\alpha$, the element constructed as the pair consisting of the bottom element $\bot$ and a proof that $\bot$ is complemented is equal to the bottom element of the sublattice of complemented elements.

Complementeds.mk_top theorem

: (⟨⊤, isComplemented_top⟩ : Complementeds α) = ⊤

Full source

theorem mk_top : (⟨⊤, isComplemented_top⟩ : Complementeds α) = ⊤ := by simp

Top Element Construction in Complemented Sublattice Equals Top

Informal description

In a bounded lattice $\alpha$, the element $\top$ (the greatest element) is complemented, and the construction of $\top$ in the sublattice of complemented elements (denoted as $\text{Complementeds}\,\alpha$) is equal to the greatest element $\top$ of $\text{Complementeds}\,\alpha$.

Complementeds.instInhabited instance

: Inhabited (Complementeds α)

Full source

instance : Inhabited (Complementeds α) := ⟨⊥⟩

Inhabitedness of the Sublattice of Complemented Elements

Informal description

For any bounded lattice $\alpha$, the sublattice of complemented elements $\text{Complementeds}\,\alpha$ is inhabited, meaning it contains at least one element.

Complementeds.instMax instance

: Max (Complementeds α)

Full source

instance : Max (Complementeds α) :=
  ⟨fun a b => ⟨a ⊔ b, a.2.sup b.2⟩⟩

Maximum Operation on Complemented Elements of a Bounded Lattice

Informal description

For any bounded lattice $\alpha$, the sublattice of complemented elements $\text{Complementeds}\,\alpha$ has a canonical maximum operation, where the maximum of two complemented elements $a$ and $b$ is given by their join $a \sqcup b$.

Complementeds.instMin instance

: Min (Complementeds α)

Full source

instance : Min (Complementeds α) :=
  ⟨fun a b => ⟨a ⊓ b, a.2.inf b.2⟩⟩

Minimum Operation on Complemented Elements in a Bounded Lattice

Informal description

For any bounded lattice $\alpha$, the sublattice of complemented elements $\text{Complementeds}\,\alpha$ has a canonical minimum operation.

Complementeds.coe_sup theorem

(a b : Complementeds α) : ↑(a ⊔ b) = (a : α) ⊔ b

Full source

@[simp, norm_cast]
theorem coe_sup (a b : Complementeds α) : ↑(a ⊔ b) = (a : α) ⊔ b := rfl

Supremum Projection for Complemented Elements in a Bounded Lattice

Informal description

For any two complemented elements $a$ and $b$ in a bounded lattice $\alpha$, the canonical projection of their supremum in the sublattice of complemented elements equals the supremum of their projections in $\alpha$, i.e., $\uparrow(a \sqcup b) = a \sqcup b$.

Complementeds.coe_inf theorem

(a b : Complementeds α) : ↑(a ⊓ b) = (a : α) ⊓ b

Full source

@[simp, norm_cast]
theorem coe_inf (a b : Complementeds α) : ↑(a ⊓ b) = (a : α) ⊓ b := rfl

Infimum of Complemented Elements in Sublattice Equals Infimum in Original Lattice

Informal description

For any two complemented elements $a$ and $b$ in a bounded lattice $\alpha$, the infimum of $a$ and $b$ in the sublattice of complemented elements is equal to the infimum of $a$ and $b$ in the original lattice $\alpha$. That is, $(a \sqcap b) = a \sqcap b$ where the left-hand side is computed in $\text{Complementeds}\,\alpha$ and the right-hand side is computed in $\alpha$.

Complementeds.mk_sup_mk theorem

 {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) : (⟨a, ha⟩ ⊔ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊔ b, ha.sup hb⟩

Full source

@[simp]
theorem mk_sup_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
    (⟨a, ha⟩⟨a, ha⟩ ⊔ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊔ b, ha.sup hb⟩ := rfl

Supremum of Complemented Elements in Sublattice Equals Complemented Supremum in Original Lattice

Informal description

Let $\alpha$ be a bounded lattice, and let $a, b \in \alpha$ be complemented elements with proofs $ha$ and $hb$ respectively. Then the supremum of the elements $\langle a, ha \rangle$ and $\langle b, hb \rangle$ in the sublattice of complemented elements is equal to $\langle a \sqcup b, ha.sup \, hb \rangle$, where $ha.sup \, hb$ is the proof that $a \sqcup b$ is complemented.

Complementeds.mk_inf_mk theorem

 {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) : (⟨a, ha⟩ ⊓ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊓ b, ha.inf hb⟩

Full source

@[simp]
theorem mk_inf_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
    (⟨a, ha⟩⟨a, ha⟩ ⊓ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊓ b, ha.inf hb⟩ := rfl

Infimum of Complemented Elements in Sublattice Equals Complemented Infimum in Original Lattice

Informal description

Let $\alpha$ be a bounded lattice, and let $a, b \in \alpha$ be complemented elements with proofs $ha$ and $hb$ respectively. Then the infimum of the elements $\langle a, ha \rangle$ and $\langle b, hb \rangle$ in the sublattice of complemented elements is equal to $\langle a \sqcap b, ha.inf \, hb \rangle$, where $ha.inf \, hb$ is the proof that $a \sqcap b$ is complemented.

Complementeds.instDistribLattice instance

: DistribLattice (Complementeds α)

Full source

instance : DistribLattice (Complementeds α) :=
  Complementeds.coe_injective.distribLattice _ coe_sup coe_inf

Distributive Lattice Structure on Complemented Elements

Informal description

The sublattice of complemented elements in a bounded lattice forms a distributive lattice.

Complementeds.disjoint_coe theorem

: Disjoint (a : α) b ↔ Disjoint a b

Full source

@[simp, norm_cast]
theorem disjoint_coe : DisjointDisjoint (a : α) b ↔ Disjoint a b := by
  rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]

Disjointness Preservation in Sublattice of Complemented Elements

Informal description

For any two elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the property of being disjoint (i.e., $a \sqcap b = \bot$) holds in $\alpha$ if and only if it holds in the sublattice.

Complementeds.codisjoint_coe theorem

: Codisjoint (a : α) b ↔ Codisjoint a b

Full source

@[simp, norm_cast]
theorem codisjoint_coe : CodisjointCodisjoint (a : α) b ↔ Codisjoint a b := by
  rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]

Codisjointness Preservation in Sublattice of Complemented Elements

Informal description

For elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the property of being codisjoint (i.e., $a \sqcup b = \top$) holds in the sublattice if and only if it holds in the original lattice $\alpha$.

Complementeds.isCompl_coe theorem

: IsCompl (a : α) b ↔ IsCompl a b

Full source

@[simp, norm_cast]
theorem isCompl_coe : IsComplIsCompl (a : α) b ↔ IsCompl a b := by
  simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]

Complement Property Preservation in Sublattice of Complemented Elements

Informal description

For elements $a$ and $b$ in the sublattice of complemented elements of a bounded lattice $\alpha$, the property of being complements (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$) holds in the sublattice if and only if it holds in the original lattice $\alpha$.

Complementeds.instComplementedLattice instance

: ComplementedLattice (Complementeds α)

Full source

instance : ComplementedLattice (Complementeds α) :=
  ⟨fun ⟨a, b, h⟩ => ⟨⟨b, a, h.symm⟩, isCompl_coe.1 h⟩⟩

Complemented Sublattice of a Bounded Lattice

Informal description

The sublattice of complemented elements in a bounded lattice forms a complemented lattice.

Main declarations