injective_of_isPartialInv_right — Mathlib

English

If f has a partial inverse g in the sense of IsPartialInv f g, and b lies in g(x) and in g(y), then x = y.

Русский

Если между f и g существует частичный обратный график, и некоторый элемент b принадлежит обоим g(x) и g(y), то x = y.

LaTeX

$$$\text{Let } H = \operatorname{IsPartialInv}(f,g).\ \forall x,y:\beta, \forall b:\alpha, b\in g(x) \land b\in g(y) \Rightarrow x=y.$$$

Lean4

theorem injective_of_isPartialInv_right {α β} {f : α → β} {g} (H : IsPartialInv f g) (x y b) (h₁ : b ∈ g x)
    (h₂ : b ∈ g y) : x = y :=
  ((H _ _).1 h₁).symm.trans ((H _ _).1 h₂)

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