mem_domain_of_mem_graph

Mathlib.LinearAlgebra.LinearPMap

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

English

If a pair (x,y) lies in the graph of f, then x belongs to the domain of f.

Русский

Если пара (x,y) принадлежит графу f, то x принадлежит области определения f.

LaTeX

$$$\text{If }(x,y) \in \mathrm{graph}(f),\; x \in \operatorname{dom}(f).$$$

Lean4

theorem mem_domain_of_mem_graph {f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y) ∈ f.graph) : x ∈ f.domain :=
  by
  rw [mem_domain_iff]
  exact ⟨y, h⟩

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

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

Разделы

Аффилиация

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