isInaccessible_def — Mathlib

English

For any cardinal c, c is inaccessible iff ℵ0 < c and c is regular and strong limit.

Русский

Для любого кардинала c недоступность эквивалентна тому, что ℵ0 < c и c регулярен и является сильным пределом.

LaTeX

$$$IsInaccessible(c) \iff \aleph_0 < c \land IsRegular(c) \land IsStrongLimit(c)$$$

Lean4

theorem isInaccessible_def {c : Cardinal} : IsInaccessible c ↔ ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c
    where
  mp h := ⟨h.aleph0_lt, h.isRegular, h.isStrongLimit⟩
  mpr := fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂.2, h₃.two_power_lt⟩

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