toRelEmbedding_injective — Mathlib

English

PrincipalSeg toRelEmbedding is injective given IsIrrefl and IsTrichotomous on β; f and g have equal toRelEmbedding implies f = g.

Русский

toRelEmbedding для PrincipalSeg инъективно при IsIrrefl и IsTrichotomous на β; равенство toRelEmbedding двух элементов влечет равенство самих элементов.

LaTeX

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

Lean4

theorem toRelEmbedding_injective [IsIrrefl β s] [IsTrichotomous β s] : Function.Injective (@toRelEmbedding α β r s) :=
  by
  rintro ⟨f, a, hf⟩ ⟨g, b, hg⟩ rfl
  congr
  refine extensional_of_trichotomous_of_irrefl s fun x ↦ ?_
  rw [← hf, hg]

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