liftQ_apply

Mathlib.LinearAlgebra.Quotient.Basic

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

English

For any p and linear map f with h: p ≤ ker f, the composed map (p.liftQ f h) ∘ p.mkQ equals f.

Русский

Пусть p — подпространство, f линейно, и h: p ≤ ker f; тогда композиция (p.liftQ f h) ∘ p.mkQ равна f.

LaTeX

$$$$ (p.liftQ f h) \\circ p.mkQ = f. $$$$

Lean4

@[simp]
theorem liftQ_apply (f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) : p.liftQ f h (Quotient.mk x) = f x :=
  rfl

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

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

Разделы

Аффилиация

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