mem_ker

Mathlib.Analysis.Normed.Group.Hom

URI: https://scilib.ai/kg/mathlib#NormedAddGroupHom.mem_ker

English

For f: NormedAddGroupHom V1 V2 and v ∈ V1, we have v ∈ ker f if and only if f(v) = 0.

Русский

Для отображения f: NormedAddGroupHom(V1,V2) и элемента v ∈ V1 верно: v ∈ ker f тогда и только тогда, когда f(v) = 0.

LaTeX

$$$v \\in \\ker f \\;\\iff\\; f(v) = 0$$$

Lean4

theorem mem_ker (v : V₁) : v ∈ f.ker ↔ f v = 0 := by rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]

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

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

Разделы

Аффилиация

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