set_eq_univ — Mathlib

English

For any subset S ⊆ ℕ, S = ℕ iff 0 ∈ S and ∀ k ∈ S, k+1 ∈ S.

Русский

Для любого подмножества S ⊆ ℕ выполняется S = ℕ тогда и только тогда, когда 0 ∈ S и ∀ k ∈ S, k+1 ∈ S.

LaTeX

$$$$ S = \mathbb{N} \iff 0 \in S \land \forall k \in \mathbb{N}, k \in S \rightarrow k+1 \in S. $$$$

Lean4

theorem set_eq_univ {S : Set ℕ} : S = Set.univ ↔ 0 ∈ S ∧ ∀ k : ℕ, k ∈ S → k + 1 ∈ S :=
  ⟨by rintro rfl; simp, fun ⟨h0, hs⟩ => Set.eq_univ_of_forall (set_induction h0 hs)⟩

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