toOrderHom_injective — Mathlib

English

The mapping that sends a RelEmbedding to its corresponding OrderHom is injective.

Русский

Отображение, переводящее RelEmbedding к соответствующему OrderHom, инъективно.

LaTeX

$$$\text{toOrderHom}$-injective: \forall f,g,\ f.toRelHom.toOrderHom = g.toRelHom.toOrderHom \Rightarrow f=g$$$

Lean4

theorem toOrderHom_injective (f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)) :
    Function.Injective (f : ((· < ·) : α → α → Prop) →r ((· < ·) : β → β → Prop)).toOrderHom := fun _ _ h =>
  f.injective h

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