iInf_eq_zero — Mathlib

English

For ENat-valued functions f, we have ⨅ i, f i = 0 iff there exists i with f i = 0.

Русский

Для ENat-значений функций f имеем ⨅ i, f i = 0 тогда и только тогда, когда существует i с f i = 0.

LaTeX

$$$\inf_i f(i) = 0 \iff \exists i, f(i) = 0$$$

Lean4

@[simp]
theorem iInf_eq_zero {f : ι → ℕ∞} : ⨅ i, f i = 0 ↔ ∃ i, f i = 0 := by
  simpa [lt_one_iff_eq_zero] using iInf_lt_iff (α := ℕ∞) (a := 1)

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