isOrdinal_iff_forall_mem_isTransitive

English

An ordinal x is exactly a transitive set and the ∈-relation on x is transitive.

Русский

Ординал x есть ровно транзитивное множество и отношение ∈ на x транзитивно.

LaTeX

$$$IsOrdinal(x) \iff (IsTrans(x) \land IsTrans\_{Subrel(\in, \in x)})$$$

Lean4

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

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