omega_succ — Mathlib

English

If n is an element of the natural numbers ω, then the successor n ∪ {n} is also in ω.

Русский

Если n принадлежит натуральным числам ω, то его переход к следующему числу n ∪ {n} также принадлежит ω.

LaTeX

$$$ n \in \omega \\Rightarrow n \cup \{ n \} \in \omega $$$

Lean4

@[simp]
theorem omega_succ {n} : n ∈ omega.{u} → insert n n ∈ omega.{u} :=
  Quotient.inductionOn n fun x ⟨⟨n⟩, h⟩ =>
    ⟨⟨n + 1⟩,
      ZFSet.exact <|
        show insert (mk x) (mk x) = insert (mk <| ofNat n) (mk <| ofNat n)
          by
          rw [ZFSet.sound h]
          rfl⟩

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