toRelEmbedding_inj — Mathlib

English

For IsIrrefl and IsTrichotomous on β, the map f.toRelEmbedding is injective, hence f=g if their embeddings agree.

Русский

При IsIrrefl и IsTrichotomous на β отображение f.toRelEmbedding инъективно, следовательно, если их вложения совпадают, то f=g.

LaTeX

$$$[IsIrrefl \\ β \\ s] [IsTrichotomous \\ β \\ s] \\Rightarrow (Injective \\\\toRelEmbedding).$$$

Lean4

@[simp]
theorem toRelEmbedding_inj [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} :
    f.toRelEmbedding = g.toRelEmbedding ↔ f = g :=
  toRelEmbedding_injective.eq_iff

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