iInf_eq_zero_iff — Mathlib

English

For a family f : ι → Cardinal, iInf f = 0 if and only if the index set ι is empty or some i satisfies f i = 0.

Русский

Для семейства f : ι → Cardinal, iInf f = 0 тогда и только тогда, когда множество индексов ι пусто или существует i, такое что f(i) = 0.

LaTeX

$$$iInf f = 0 \iff IsEmpty\, ι \lor \exists i, f(i) = 0$$$

Lean4

theorem iInf_eq_zero_iff {ι : Sort*} {f : ι → Cardinal} : (⨅ i, f i) = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0 := by
  simp [iInf, sInf_eq_zero_iff]

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