inf_eq_bot_of_ne — Mathlib

English

Two distinct atoms have magnetic infimum equal to bottom; i.e., a ⊓ b = ⊥ when a ≠ b.

Русский

Два различных атома имеют минимум равным низу; то есть a ⊓ b = ⊥ при a ≠ b.

LaTeX

$$$ \\text{IsAtom}(a) \\rightarrow \\text{IsAtom}(b) \\rightarrow a \\neq b \\rightarrow a \\sqcap b = \\bot.$$$

Lean4

@[deprecated disjoint_of_ne (since := "2025-07-11")]
theorem inf_eq_bot_of_ne (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : a ⊓ b = ⊥ :=
  hab.not_le_or_not_ge.elim (ha.lt_iff.1 ∘ inf_lt_left.2) (hb.lt_iff.1 ∘ inf_lt_right.2)

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