covBy_iff_coatom_Iic — Mathlib

English

If a ≤ b, then a covers b in the ambient order if and only if ⟨a, h⟩ is a coatom in Set.Iic b.

Русский

Если a ≤ b, то a покрывает b в исходном порядке тогда, когда ⟨a, h⟩ является коатомом в Set.Iic b.

LaTeX

$$$ (\\forall h:\\, a \\le b), a \\lessdot b \\iff \\mathrm{IsCoatom}(\\langle a, h \\rangle).$$$

Lean4

theorem covBy_iff_coatom_Iic (h : a ≤ b) : a ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b) := by simp

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