ofAntisymmetrization_lt_ofAntisymmetrization_iff

English

Let α be a preorder. The antisymmetrization map also reflects the strict order: for all a,b in Antisymmetrization α (≤), a < b iff the quotient representatives satisfy corresponding inequality.

Русский

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

LaTeX

$$$\\forall a,b:\\ a < b \\iff \\text{(representatives of } a,b \\text{ satisfy the order)}$$$

Lean4

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

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