toAntisymmetrization_lt_toAntisymmetrization_iff

English

Let α be a preorder. The strict order is preserved and reflected by the antisymmetrization map: for all a,b in α, [a] < [b] iff a < b.

Русский

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

LaTeX

$$$\\forall a,b\\in \\alpha:\\ [a] < [b] \\iff a < b$$$

Lean4

@[simp]
theorem toAntisymmetrization_lt_toAntisymmetrization_iff :
    toAntisymmetrization (α := α) (· ≤ ·) a < toAntisymmetrization (α := α) (· ≤ ·) b ↔ a < b :=
  Iff.rfl

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