inclusion_inj

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#Submonoid.inclusion_inj

← MathLib Explorer

English

For x,y ∈ S, inclusion(h)(x) = inclusion(h)(y) iff x = y.

Русский

Для x,y ∈ S: inclusion(h)(x) = inclusion(h)(y) тогда и только тогда, когда x = y.

LaTeX

$$$ \mathrm{inclusion}(h)(x) = \mathrm{inclusion}(h)(y) \leftrightarrow x = y $$$

Lean4

@[to_additive (attr := simp)]
theorem inclusion_inj {S T : Submonoid M} (h : S ≤ T) {x y : S} : inclusion h x = inclusion h y ↔ x = y :=
  (inclusion_injective h).eq_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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