disjoint_self — Mathlib

English

Disjoint(a,a) holds if and only if a equals the bottom element ⊥.

Русский

Disjoint(a,a) выполняется тогда и только тогда, когда a = ⊥.

LaTeX

$$$Disjoint(a,a) \\iff a = \\bot$$$

Lean4

@[simp]
theorem disjoint_self : Disjoint a a ↔ a = ⊥ :=
  ⟨fun hd ↦ bot_unique <| hd le_rfl le_rfl, fun h _ ha _ ↦ ha.trans_eq h⟩
    /- TODO: Rename `Disjoint.eq_bot` to `Disjoint.inf_eq` and `Disjoint.eq_bot_of_self` to
    `Disjoint.eq_bot` -/

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