inclusion_injective

Mathlib.Algebra.Module.Submodule.LinearMap

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

English

For p ⊆ p' and h, the composition q.subtype ∘ inclusion(h) equals p.subtype.

Русский

При p ⊆ p' и некотором h композиция q.subtype ∘ inclusion(h) равна p.subtype.

LaTeX

$$q.\\text{subtype} \\circ (Submodule.inclusion h) = p.\\text{subtype}$$

Lean4

theorem inclusion_injective (h : p ≤ p') : Function.Injective (inclusion h) := fun _ _ h =>
  Subtype.val_injective (Subtype.mk.inj h)

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

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

Разделы

Аффилиация

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