isOrdinal_iff_isTrichotomous — Mathlib

English

An ordinal x is exactly transitive and trichotomous under membership.

Русский

Ординал x есть транзитивный и тричотомный по отношению принадлежности.

LaTeX

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

Lean4

/-- An ordinal is a transitive set, trichotomous under membership. -/
theorem _root_.ZFSet.isOrdinal_iff_isTrichotomous :
    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x))
    where
  mp h := ⟨h.isTransitive, h.isTrichotomous⟩
  mpr := by
    rintro ⟨h₁, h₂⟩
    rw [isOrdinal_iff_isTrans]
    refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩
    obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
    · exact hyw
    · cases asymm hyz hzw
    · cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

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