Theorems · Theorem · logic and foundations
ZFSet.isOrdinal_iff_isTrichotomous
Deprecated since 2026-01-24Use ZFSet.isOrdinal_iff_trichotomous instead.
∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)Alias of ZFSet.isOrdinal_iff_trichotomous.
An ordinal is a transitive set, trichotomous under membership.
- Defined in
- Mathlib.SetTheory.ZFC.Ordinal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZFSetstatement · cited by 259
- Subrelstatement · cited by 53
- ZFSet.IsOrdinalstatement · cited by 34
- ZFSet.IsTransitivestatement · cited by 22
- ZFSet.isOrdinal_iff_trichotomousproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.