bot_covBy_iff — Mathlib

English

Let α be a poset with a bottom element. Then ⊥ is covered by a if and only if a is an atom.

Русский

Пусть α — частично упорядоченное множество с нулём. ⊥ покрывается элементом a тогда, когда a является атомом.

LaTeX

$$$ \\bot \\lessdot a \\iff \\text{IsAtom}(a) $$$

Lean4

@[simp]
theorem bot_covBy_iff : ⊥ ⋖ a ↔ IsAtom a := by simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not]

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