ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
letI := a.totalSpaceTopology
case intro.intro
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he')
  e.source (a.isOpen_source e)
case intro.intro
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (u ∩ e'.target)
case intro.intro
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (e'.target ∩ ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source)
rw [inter_comm, hu2]
no goals
case intro.intro
ι : Type ?u.58328
B : Type u_1
F : Type u_2
X : Type ?u.58337
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑(LocalEquiv.symm e'.toLocalEquiv) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (u ∩ e'.target)
exact hu1.inter e'.open_target