eventually_left_inverse — Mathlib

English

For each x in the source, there is a neighborhood of x on which e symm composed with e is the identity.

Русский

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

LaTeX

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

Lean4

theorem eventually_left_inverse {x} (hx : x ∈ e.source) : ∀ᶠ y in 𝓝 x, e.symm (e y) = y :=
  (e.open_source.eventually_mem hx).mono e.left_inv'

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