English
There exists a PartialOrder structure on the antisymmetrization of α with respect to ≤, induced by the quotient construction.
Русский
Существует структура частичного порядка на антисимметризации α по отношению к ≤, получаемая как фактор-множество.
LaTeX
$$$\\text{PartialOrder}(\\text{Antisymmetrization}(α, ≤))$$$
Lean4
instance instPartialOrderAntisymmetrization : PartialOrder (Antisymmetrization α (· ≤ ·))
where
le :=
Quotient.lift₂ (· ≤ ·) fun (_ _ _ _ : α) h₁ h₂ =>
propext ⟨fun h => h₁.2.trans <| h.trans h₂.1, fun h => h₁.1.trans <| h.trans h₂.2⟩
lt :=
Quotient.lift₂ (· < ·) fun (_ _ _ _ : α) h₁ h₂ =>
propext ⟨fun h => h₁.2.trans_lt <| h.trans_le h₂.1, fun h => h₁.1.trans_lt <| h.trans_le h₂.2⟩
le_refl a := Quotient.inductionOn' a le_refl
le_trans a b c := Quotient.inductionOn₃' a b c fun _ _ _ => le_trans
lt_iff_le_not_ge a b := Quotient.inductionOn₂' a b fun _ _ => lt_iff_le_not_ge
le_antisymm a b := Quotient.inductionOn₂' a b fun _ _ hab hba => Quotient.sound' ⟨hab, hba⟩
