inf_eq_bot_iff — Mathlib

English

For atoms a and any b, a ⊓ b = ⊥ if and only if not a ≤ b.

Русский

Для атома a и любого b, a ⊓ b = ⊥ тогда, когда не выполняется a ≤ b.

LaTeX

$$$ \\mathrm{IsAtom}(a) \\rightarrow (a \\wedge b = \\bot \\leftrightarrow \\lnot a \\le b).$$$

Lean4

@[deprecated not_le_iff_disjoint (since := "2025-07-11")]
theorem inf_eq_bot_iff (ha : IsAtom a) : a ⊓ b = ⊥ ↔ ¬a ≤ b :=
  by
  by_cases hb : b = ⊥
  · simpa [hb] using ha.1
  · exact ⟨fun h ↦ inf_lt_left.mp (h ▸ bot_lt ha), fun h ↦ ha.2 _ (inf_lt_left.mpr h)⟩

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