extend_left_inv — Mathlib

English

For every x in the source of f, applying the extended map and then its inverse brings you back to x.

Русский

Для каждого x из источника f применение расширённого отображения и затем его обратного отображения возвращает x.

LaTeX

$$$ (f \\extend I)^{-1}((f \\extend I)(x)) = x \\quad \\text{for all } x \\in f.source. $$$

Lean4

theorem extend_left_inv {x : M} (hxf : x ∈ f.source) : (f.extend I).symm (f.extend I x) = x :=
  (f.extend I).left_inv <| by rwa [f.extend_source]

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