mem_domain_iff_of_eq_graph — Mathlib

English

If two linear partial maps have the same graph, then their domains coincide.

Русский

Если два линейных частичных отображения имеют одинаковый график, то их области определения совпадают.

LaTeX

$$$ f.graph = g.graph \\Rightarrow \\forall x \\in E,\\ x \\in \\mathrm{domain}(f) \\iff x \\in \\mathrm{domain}(g) $$$

Lean4

theorem mem_domain_iff_of_eq_graph {f g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} : x ∈ f.domain ↔ x ∈ g.domain :=
  by simp_rw [mem_domain_iff, h]

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