ofAntisymmetrization_le_ofAntisymmetrization_iff

English

Let α be a preorder. The map from Antisymmetrization α (≤) to α preserves and reflects order: for any a,b in Antisymmetrization α (≤), a ≤ b in Antisymmetrization iff the images satisfy a ≤ b in α.

Русский

Пусть α — частично упорядоченное множество. Отображение из антисимметризации α в α сохраняет и отражает порядок: для любых a,b в антисимметризации выполняется a ≤ b тогда и только тогда, когда их образы удовлетворяют a ≤ b в α.

LaTeX

$$$\\forall a,b:\\ a,b \\in \\text{Antisymmetrization}(\\alpha, {\\le}):\\ \\text{ofAntisymmetrization}(\\le)\\ a \\le \\text{ofAntisymmetrization}(\\le)\\ b \\iff a \\le b$$$

Lean4

@[simp]
theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
    ofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b :=
  (Quotient.outRelEmbedding _).map_rel_iff

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