#linearordering — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #linearordering, aggregated by home.social.
-
@FishFace Update:
What I refer to as EScbO is usually called #LO the #LinearOrdering principle.
⊢ ∃y ∀a ∈ x ∀b ∈ x ∀c ∈ x (¬ aya ∧ ((ayb ∧ byc) → ayc) ∧ (ayb ∨ a = b ∨ bya))
or using abbreviations in #Metamath
⊢ ∃y y Or xI think AC implies LO, but LO is independent of DC and CC.