sInf_le — Mathlib

English

In a Coframe, the infimum sInf s is below a if and only if there exists b ∈ s with b ≤ a, given a is a coatom.

Русский

В кофрагме нижняя грань множества s ниже a тогда, когда существует b ∈ s такой, что b ≤ a, при условии, что a — коатом.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow (\\mathrm{sInf}\, s \\le a \\iff \\exists b \\in s, b \\le a).$$$

Lean4

protected theorem sInf_le (ha : IsCoatom a) : sInf s ≤ a ↔ ∃ b ∈ s, b ≤ a := by simp [sInf_eq_iInf', ha.iInf_le]

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