domRestrict_domain

Mathlib.LinearAlgebra.LinearPMap

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

English

The domain of f restricted to S equals S ∩ dom(f).

Русский

Область определения отображения f, ограниченного до S, равна S ∩ dom(f).

LaTeX

$$$\operatorname{dom}(f|_S) = S \cap \operatorname{dom}(f).$$$

Lean4

@[simp]
theorem domRestrict_domain (f : E →ₗ.[R] F) {S : Submodule R E} : (f.domRestrict S).domain = S ⊓ f.domain :=
  rfl

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

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

Разделы

Аффилиация

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