toEmbedding_inj

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelEmbedding.toEmbedding_inj

English

Two RelEmbedding are equal iff their toEmbedding components are equal.

Русский

Два RelEmbedding равны тогда и только тогда, когда их toEmbedding равны.

LaTeX

$$$\forall f,g : r \hookrightarrow r s,\ f.toEmbedding = g.toEmbedding \iff f = g$$$

Lean4

@[simp]
theorem toEmbedding_inj {f g : r ↪r s} : f.toEmbedding = g.toEmbedding ↔ f = g :=
  toEmbedding_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru