instSub

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.instSub

English

If f = g, then for every x in N, f x = g x.

Русский

Если f = g, то для любого x ∈ N выполняется f(x) = g(x).

LaTeX

$$theorem congr_fun {f g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) : f x = g x := h ▸ rfl$$

Lean4

instance : Sub (M →ₗ⁅R,L⁆ N) where sub f g := { (f : M →ₗ[R] N) - (g : M →ₗ[R] N) with map_lie' := by simp }

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

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

Разделы

Аффилиация

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