iInf_coe_lt_top — Mathlib

English

For any f:ι→α, the infimum of the WithTop-coerced values is strictly below top exactly when ι is nonempty.

Русский

Для любого f:ι→α инфимуум приведенных значений в WithTop строго меньше топа тогда, когда ι непусто.

LaTeX

$$$\\bigwedge_{i} (f(i) : \\mathrm{WithTop}\\,\\alpha) < \\top \\iff \\mathrm{Nonempty}(\\iota)$$$

Lean4

theorem iInf_coe_lt_top : ⨅ i, (f i : WithTop α) < ⊤ ↔ Nonempty ι := by
  rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]

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