iInf_coe_eq_top — Mathlib

English

Characterizes iInf over WithTop-coerced values: it equals top iff the index set is empty; equivalently, iInf (f) = top iff ι is empty.

Русский

Характеризует инфимума в WithTop: он равен топу тогда, когда индексное множество пусто.

LaTeX

$$$iInf\\{ f(x) : x\\in \\iota\\} = \\top \\iff \\mathrm{IsEmpty}(\\iota)$$$

Lean4

theorem iInf_coe_eq_top : ⨅ x, (f x : WithTop α) = ⊤ ↔ IsEmpty ι := by simp [isEmpty_iff]

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