codisjoint_self — Mathlib

English

Codisjoint a a is equivalent to a being the top element.

Русский

Codisjoint a a эквивалентно тому, что a = ⊤.

LaTeX

$$$\operatorname{Codisjoint}(a,a) \iff a = \top$$$

Lean4

@[simp]
theorem codisjoint_self : Codisjoint a a ↔ a = ⊤ :=
  ⟨fun hd ↦ top_unique <| hd le_rfl le_rfl, fun h _ ha _ ↦ h.symm.trans_le ha⟩
    /- TODO: Rename `Codisjoint.eq_top` to `Codisjoint.sup_eq` and `Codisjoint.eq_top_of_self` to
    `Codisjoint.eq_top` -/

Похожие утверждения