sInf_eq_zero_iff — Mathlib

English

For any set s of cardinals, the infimum sInf s equals 0 if and only if s is empty or contains a zero.

Русский

Для множества s кардиналов, sInf s равно нулю тогда и только тогда, когда s пусто или содержит нуль.

LaTeX

$$$sInf\,s = 0 \iff s = \emptyset \lor \exists a \in s, a = 0$$$

Lean4

theorem sInf_eq_zero_iff {s : Set Cardinal} : sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases s.eq_empty_or_nonempty with rfl | hne
    · exact Or.inl rfl
    · exact Or.inr ⟨sInf s, csInf_mem hne, h⟩
  · rcases h with rfl | ⟨a, ha, rfl⟩
    · exact Cardinal.sInf_empty
    · exact eq_bot_iff.2 (csInf_le' ha)

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