Lean4
/-- For `Ordinal`:
* less-equal is defined such that well orders `r` and `s` satisfy `type r ≤ type s` if there exists
a function embedding `r` as an *initial* segment of `s`.
* less-than is defined such that well orders `r` and `s` satisfy `type r < type s` if there exists
a function embedding `r` as a *principal* segment of `s`.
Note that most of the relevant results on initial and principal segments are proved in the
`Order.InitialSeg` file.
-/
instance partialOrder : PartialOrder Ordinal
where
le a
b :=
Quotient.liftOn₂ a b (fun ⟨_, r, _⟩ ⟨_, s, _⟩ => Nonempty (r ≼i s)) fun _ _ _ _ ⟨f⟩ ⟨g⟩ =>
propext
⟨fun ⟨h⟩ => ⟨f.symm.toInitialSeg.trans <| h.trans g.toInitialSeg⟩, fun ⟨h⟩ =>
⟨f.toInitialSeg.trans <| h.trans g.symm.toInitialSeg⟩⟩
lt a
b :=
Quotient.liftOn₂ a b (fun ⟨_, r, _⟩ ⟨_, s, _⟩ => Nonempty (r ≺i s)) fun _ _ _ _ ⟨f⟩ ⟨g⟩ =>
propext
⟨fun ⟨h⟩ => ⟨PrincipalSeg.relIsoTrans f.symm <| h.transRelIso g⟩, fun ⟨h⟩ =>
⟨PrincipalSeg.relIsoTrans f <| h.transRelIso g.symm⟩⟩
le_refl := Quot.ind fun ⟨_, _, _⟩ => ⟨InitialSeg.refl _⟩
le_trans a b c := Quotient.inductionOn₃ a b c fun _ _ _ ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩
lt_iff_le_not_ge a
b :=
Quotient.inductionOn₂ a b fun _ _ =>
⟨fun ⟨f⟩ => ⟨⟨f⟩, fun ⟨g⟩ => (f.transInitial g).irrefl⟩, fun ⟨⟨f⟩, h⟩ =>
f.principalSumRelIso.recOn (fun g => ⟨g⟩) fun g => (h ⟨g.symm.toInitialSeg⟩).elim⟩
le_antisymm a b := Quotient.inductionOn₂ a b fun _ _ ⟨h₁⟩ ⟨h₂⟩ => Quot.sound ⟨InitialSeg.antisymm h₁ h₂⟩
