iInf_le — Mathlib

English

In a Coframe, the infimum of a family f is below a if and only if there exists an index i with f(i) ≤ a, provided a is a coatom.

Русский

В кофраме наименьшее (iInf) множества f ниже a тогда и только тогда, существует индекс i, для которого f(i) ≤ a, если a — коатом.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow (\\mathrm{iInf}\, f \\le a \\iff \\exists i, f(i) \\le a).$$$

Lean4

protected theorem iInf_le (ha : IsCoatom a) : iInf f ≤ a ↔ ∃ i, f i ≤ a :=
  IsAtom.le_iSup (α := αᵒᵈ) ha

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