domRestrict_le

Mathlib.LinearAlgebra.LinearPMap

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

English

The restricted map f|_S is less than or equal to f in the natural partial order on LinearPMaps.

Русский

Ограниченное отображение f|_S меньше или равно f в естественном частичном порядке на LinearPMap.

LaTeX

$$$f|_S \le f$$$

Lean4

theorem domRestrict_le {f : E →ₗ.[R] F} {S : Submodule R E} : f.domRestrict S ≤ f :=
  ⟨by simp, fun _ _ hxy => domRestrict_apply hxy⟩

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

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

Разделы

Аффилиация

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