notMem_of_lt_sInf — Mathlib

English

If m < sInf s, then m ∉ s.

Русский

Если m меньше sInf s, то m не принадлежит s.

LaTeX

$$$\\forall s \\subseteq \\mathbb{N}, \\forall m \\in \\mathbb{N}, \\ m < sInf(s) \\Rightarrow m \\notin s$$$

Lean4

theorem notMem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s := by
  classical
    cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

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