extend_left_inv' — Mathlib

English

For any subset t of the source, the left-inverse composition maps t to itself via its image under the extended chart.

Русский

Для любого подмножества t ⊆ source левая композиция отображения возвращает t через образ под расширенным чартом.

LaTeX

$$$ ((f \\extend I)^{-1} \\circ (f \\extend I)) [t] = t \\quad \\text{for } t \\subseteq f.source. $$$

Lean4

/-- Variant of `f.extend_left_inv I`, stated in terms of images. -/
theorem extend_left_inv' (ht : t ⊆ f.source) : ((f.extend I).symm ∘ (f.extend I)) '' t = t :=
  EqOn.image_eq_self (fun _ hx ↦ f.extend_left_inv (ht hx))

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