toAntisymmetrization_le_toAntisymmetrization_iff

English

Let α be a preorder. The canonical map i: α → Antisymmetrization α (≤) embeds α into its antisymmetrization, preserving and reflecting the order: for all a,b in α, [a] ≤ [b] iff a ≤ b. (Here [a] denotes the class of a in the antisymmetrization.)

Русский

Пусть α — частично упорядоченное множество. Каноническое отображение i: α → Антисимметризация α (≤) является вложением порядка: для любых a,b ∈ α выполняется [a] ≤ [b] тогда и только тогда, когда a ≤ b. Здесь [a] обозначает класс a в антисимметризации.

LaTeX

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

Lean4

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

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