sInf_upward_closed_eq_succ_iff — Mathlib

English

For an upward closed set s, sInf s = k+1 holds iff k+1 ∈ s and k ∉ s.

Русский

Для восходящего множества s, sInf s = k+1 эквивалентно тому, что k+1 ∈ s и k ∉ s.

LaTeX

$$$$ sInf(s) = k+1 \iff (k+1) \in s \ \\wedge\ k \notin s. $$$$

Lean4

theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) (k : ℕ) :
    sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s := by
  classical
  constructor
  · intro H
    rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
    · exact ⟨le_rfl, k.not_succ_le_self⟩
    · exact k
    · assumption
  · rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

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