isOrdinal_iff_isWellOrder — Mathlib

English

An ordinal x is well-ordered by ∈ and vice versa.

Русский

Ординал эквивалентно тому, что он упорядочен по ∈, и обратно.

LaTeX

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

Lean4

/-- An ordinal is a transitive set, well-ordered under membership. -/
theorem _root_.ZFSet.isOrdinal_iff_isWellOrder :
    x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder _ (Subrel (· ∈ ·) (· ∈ x)) :=
  by
  use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩
  rintro ⟨h₁, h₂⟩
  refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩
  infer_instance

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