toPreorder_injective — Mathlib

English

Two PartialOrders on α are equal if their underlying Preorder structures coincide.

Русский

Две частичные порядки на α равны, если их базовые структуры предупорядоченности совпадают.

LaTeX

$$$ \forall A,B:\text{PartialOrder}(\alpha),\ (toPreorder\,A = toPreorder\,B) \rightarrow A = B $$$

Lean4

@[ext]
theorem toPreorder_injective : Function.Injective (@PartialOrder.toPreorder α) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; congr

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