compHomeomorph — Mathlib

English

Auxiliary lemma for the symmetric application of preimageHomeomorph.

Русский

Вспомогательная лемма для симметричного применения предобразного гомеоморфизма.

LaTeX

$$$ (preimageHomeomorph_symm_apply.aux e hb) p.2 $$$

Lean4

/-- Composition of a `Trivialization` and a `Homeomorph`. -/
protected def compHomeomorph {Z' : Type*} [TopologicalSpace Z'] (h : Z' ≃ₜ Z) : Trivialization F (proj ∘ h)
    where
  toOpenPartialHomeomorph := h.toOpenPartialHomeomorph.trans e.toOpenPartialHomeomorph
  baseSet := e.baseSet
  open_baseSet := e.open_baseSet
  source_eq := by simp [source_eq, preimage_preimage, Function.comp_def]
  target_eq := by simp [target_eq]
  proj_toFun p
    hp := by
    have hp : h p ∈ e.source := by simpa using hp
    simp [hp]

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