continuousOn_symm — Mathlib

English

As above, TotalSpace.mk b (e.symm b y) equals the inverse image under the open partial homeomorph.

Русский

Как выше, TotalSpace.mk b (e.symm b y) равняется обратному изображению под открытым частичным гомоморфом.

LaTeX

$$$TotalSpace.mk\\, b\\, (e.symm\\, b\\, y) = e.toOpenPartialHomeomorph.symm (b, y)$$$

Lean4

theorem continuousOn_symm (e : Trivialization F (π F E)) :
    ContinuousOn (fun z : B × F => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ) :=
  by
  have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F), TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toOpenPartialHomeomorph.symm z :=
    by
    rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
    rw [e.mk_symm hx]
  refine ContinuousOn.congr ?_ this
  rw [← e.target_eq]
  exact e.toOpenPartialHomeomorph.continuousOn_symm

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