Lean4
/-- If `x` is evenly covered by `f` with nonempty fiber `I`, then we can construct a
trivialization of `f` at `x` with fiber `I`. -/
noncomputable def toTrivialization' {x : X} [Nonempty I] (h : IsEvenlyCovered f x I) : Trivialization I f :=
by
choose _ U hxU hU hfU H hH using h
classical
exact
{ toFun e := if he : f e ∈ U then ⟨(H ⟨e, he⟩).1, (H ⟨e, he⟩).2⟩ else ⟨x, Classical.arbitrary I⟩
invFun xi := H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)
source := f ⁻¹' U
target := U ×ˢ Set.univ
map_source' e (he : f e ∈ U) := by simp [he]
map_target' _ _ := Subtype.coe_prop _
left_inv' e (he : f e ∈ U) := by simp [he]
right_inv' xi := by rintro ⟨hx, -⟩; simpa [hx] using fun h ↦ (h (H.symm _).2).elim
open_source := hfU
open_target := hU.prod isOpen_univ
continuousOn_toFun :=
continuousOn_iff_continuous_restrict.mpr <|
((continuous_subtype_val.prodMap continuous_id).comp H.continuous).congr fun ⟨e, (he : f e ∈ U)⟩ ↦ by
simp [Prod.map, he]
continuousOn_invFun :=
continuousOn_iff_continuous_restrict.mpr <|
((continuous_subtype_val.comp H.symm.continuous).comp
(by fun_prop : Continuous fun ui ↦ ⟨⟨_, ui.2.1⟩, ui.1.2⟩)).congr
fun ⟨⟨x, i⟩, ⟨hx, _⟩⟩ ↦ by simp [hx]
baseSet := U
open_baseSet := hU
source_eq := rfl
target_eq := rfl
proj_toFun e (he : f e ∈ U) := by simp [he, hH] }
