eq_Ici_of_nonempty_of_upward_closed

English

If s is nonempty and upward closed, then s equals {n ∈ ℕ: n ≥ sInf s}.

Русский

Если s непусто и восходяще замкнуто, то s = {n ∈ ℕ : n ≥ sInf s}.

LaTeX

$$$\\text{If } s \\neq \\emptyset \\text{ and upwardClosed}(s), \\ s = \\{ n \\in \\mathbb{N} : n \ge sInf(s) \\\\}.$$$

Lean4

theorem eq_Ici_of_nonempty_of_upward_closed {s : Set ℕ} (hs : s.Nonempty)
    (hs' : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) : s = Ici (sInf s) :=
  ext fun n ↦ ⟨fun H ↦ Nat.sInf_le H, fun H ↦ hs' (sInf s) n H (sInf_mem hs)⟩

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