eventually_right_inverse' — Mathlib

English

If x ∈ e.source, then near e(x) in Y, e ∘ e^{-1} is the identity on a neighborhood of e(x).

Русский

Если x ∈ e.source, то возле e(x) в Y отображение e ∘ e^{-1} равно тождественному на окрестности e(x).

LaTeX

$$$\forall x\in e.source, \forall \text{neighborhood } V \ni e(x), \forall y\in V, e(e^{-1}(y))=y$$$

Lean4

theorem eventually_right_inverse' {x} (hx : x ∈ e.source) : ∀ᶠ y in 𝓝 (e x), e (e.symm y) = y :=
  e.eventually_right_inverse (e.map_source hx)

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