sInf_eq_zero — Mathlib

English

For any s ⊆ ℕ, sInf s = 0 if and only if 0 ∈ s or s = ∅.

Русский

Для любого s ⊆ ℕ, sInf s = 0 тогда и только тогда, когда 0 ∈ s или s = ∅.

LaTeX

$$$sInf(s) = 0 \iff 0 \in s \lor s = \emptyset$$$

Lean4

@[simp]
theorem sInf_eq_zero {s : Set ℕ} : sInf s = 0 ↔ 0 ∈ s ∨ s = ∅ := by
  cases eq_empty_or_nonempty s with
  | inl h =>
    subst h
    simp only [or_true, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

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