mem_graph_iff — Mathlib

English

For a linear map f, an element x belongs to its graph precisely when the second component equals the image of the first, i.e., (m, m2) ∈ graph(f) iff m2 = f(m).

Русский

Пусть линейное отображение f. Тогда элемент x принадлежит графику, если и только если вторая компонента равна изображению первой: (m, m₂) ∈ graph(f) ↔ m₂ = f(m).

LaTeX

$$$x \\in \\text{graph}(f) \\iff x_2 = f(x_1)$$$

Lean4

@[simp]
theorem mem_graph_iff (x : M × M₂) : x ∈ f.graph ↔ x.2 = f x.1 :=
  Iff.rfl

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