inclusion_injective

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.inclusion_injective

English

The inclusion map from S to T is injective when S ≤ T.

Русский

Включение из S в T инъективно при S ≤ T.

LaTeX

$$$\text{inclusion}(h)$ is injective, where $h$ encodes $S \le T$$$

Lean4

theorem inclusion_injective : Function.Injective (inclusion h) := fun _ _ => Subtype.ext ∘ Subtype.mk.inj

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

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

Разделы

Аффилиация

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