eventually_left_inverse' — Mathlib

English

For each x in the target, there is a neighborhood around e(x) where e composed with its inverse is the identity.

Русский

Для каждого x в целевой области существует окрестность e(x), на которой e∘e^{-1} является тождественной.

LaTeX

$$$\forall x\in e.target, \exists V\ni e(x): \forall y\in V, e(e^{-1}(y))=y$$$

Lean4

theorem eventually_left_inverse' {x} (hx : x ∈ e.target) : ∀ᶠ y in 𝓝 (e.symm x), e.symm (e y) = y :=
  e.eventually_left_inverse (e.map_target hx)

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