mem_graph_snd_inj — Mathlib

English

If x in the restricted domain corresponds to y in dom(f) with the same underlying value, then the restricted map evaluates to f(y).

Русский

Если элемент x в ограниченной области соответствует y в dom(f) с тем же базовым значением, то ограниченное отображение равно f(y).

LaTeX

$$$(f|_S)(x) = f(y) \quad\text{whenever } (x:E)=y \text{ and } x\in S\cap\operatorname{dom}(f).$$$

Lean4

theorem mem_graph_snd_inj (f : E →ₗ.[R] F) {x y : E} {x' y' : F} (hx : (x, x') ∈ f.graph) (hy : (y, y') ∈ f.graph)
    (hxy : x = y) : x' = y' := by grind [mem_graph_iff]

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