le_graph_iff

Mathlib.LinearAlgebra.LinearPMap

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

English

For linear partial maps, the graph order relation is equivalent to the map order relation.

Русский

Для линейных частичных отображений графовый порядок эквивалентен порядку отображения.

LaTeX

$$f.graph \\le g.graph \\leftrightarrow f \\le g$$

Lean4

theorem le_graph_iff {f g : E →ₗ.[R] F} : f.graph ≤ g.graph ↔ f ≤ g :=
  ⟨le_of_le_graph, le_graph_of_le⟩

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

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

Разделы

Аффилиация

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