iInf_coe_ne_top — Mathlib

English

The iInf over ENat-casts is not top exactly when there exists at least one index: iInf (f i).cast ≠ ⊤ iff ι is nonempty.

Русский

iInf над ENat-cast не равна ⊤ тогда и только тогда, когда множество индексов непусто.

LaTeX

$$$$ \\mathrm{iInf}_{i} (f(i)^{\\ cast}) \\neq \\top \\iff \\mathrm{Nonempty}(i) $$$$

Lean4

theorem iInf_coe_ne_top : ⨅ i, (f i : ℕ∞) ≠ ⊤ ↔ Nonempty ι := by rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]

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