ι : Type ?u.6444
B : Type u_1
F : Type ?u.6450
X : Type ?u.6453
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_2
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (Sigma.fst ⁻¹' {x})
ι : Type ?u.6444
B : Type u_1
F : Type ?u.6450
X : Type ?u.6453
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_2
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (range (totalSpaceMk x))
rw [range_sigmaMk]
no goals
ι : Type ?u.6444
B : Type u_1
F : Type ?u.6450
X : Type ?u.6453
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_2
inst✝³ : TopologicalSpace (TotalSpace E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed (Sigma.fst ⁻¹' {x})
exact isClosed_singleton.preimage <| continuous_proj F E