mem_inverse_graph — Mathlib

English

The graph of the inverse is characterized by the property that (f x, x) lies in the inverse graph when x ∈ domain.

Русский

Граф обратного задаётся свойством: (f x, x) ∈ граф обратного, когда x ∈ область определения.

LaTeX

$$x ∈ f.domain → (f x, x) ∈ (inverse f).graph$$

Lean4

theorem mem_inverse_graph (x : f.domain) : (f x, (x : E)) ∈ (inverse f).graph :=
  by
  simp only [inverse_graph hf, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
  exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩

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