hasCore_def

Mathlib.Topology.Algebra.Module.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.hasCore_def

English

If f.HasCore S, then the closure of f restricted to S equals f.

Русский

Если у f есть ядро (core) на S, то замыкание ограниченного f на S равно f.

LaTeX

$$$f.HasCore S \Rightarrow (f.domRestrict S).closure = f$$$

Lean4

theorem hasCore_def {f : E →ₗ.[R] F} {S : Submodule R E} (h : f.HasCore S) : (f.domRestrict S).closure = f :=
  h.2

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

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

Разделы

Аффилиация

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