isOrdinal_iff_forall_mem_isOrdinal

English

An ordinal is a transitive set of transitive sets.

Русский

Ординал является транзитивным множеством транситивных множеств.

LaTeX

$$$IsOrdinal(x) \iff (IsTransitive(x) \land \forall y \in x, IsTransitive(y))$$$

Lean4

/-- An ordinal is a transitive set of ordinals. -/
theorem _root_.ZFSet.isOrdinal_iff_forall_mem_isOrdinal : x.IsOrdinal ↔ x.IsTransitive ∧ ∀ y ∈ x, y.IsOrdinal
    where
  mp h := ⟨h.isTransitive, fun _ ↦ h.mem⟩
  mpr := fun ⟨h₁, h₂⟩ ↦ isOrdinal_iff_forall_mem_isTransitive.2 ⟨h₁, fun y hy ↦ (h₂ y hy).isTransitive⟩

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