apply_ofInjective_symm — Mathlib

English

For x in f.range, applying f to the preimage under the inverse recovers x.

Русский

Для x ∈ образа f применение f к предобразу через обратное возвращает x.

LaTeX

$$$$ f((\\mathrm{ofInjective hf})^{-1}(x)) = x, \\quad x \\in f(G) $$$$

Lean4

@[to_additive (attr := simp)]
theorem apply_ofInjective_symm {f : G →* N} (hf : Function.Injective f) (x : f.range) :
    f ((ofInjective hf).symm x) = x :=
  Subtype.ext_iff.1 <| (ofInjective hf).apply_symm_apply x

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