α : Type u
β : Type v
γ : Type ?u.527967
δ : Type ?u.527970
ε : Type ?u.527973
ζ : Type ?u.527976
ι : Type u_1
κ : Type ?u.527982
σ : ι → Type u_2
τ : κ → Type ?u.527992
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), Sigma.fst ⁻¹' {i})
α : Type u
β : Type v
γ : Type ?u.527967
δ : Type ?u.527970
ε : Type ?u.527973
ζ : Type ?u.527976
ι : Type u_1
κ : Type ?u.527982
σ : ι → Type u_2
τ : κ → Type ?u.527992
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (Sigma.fst ⁻¹' s)
rw [← biUnion_of_singleton s, preimage_iUnion₂]
α : Type u
β : Type v
γ : Type ?u.527967
δ : Type ?u.527970
ε : Type ?u.527973
ζ : Type ?u.527976
ι : Type u_1
κ : Type ?u.527982
σ : ι → Type u_2
τ : κ → Type ?u.527992
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), range (Sigma.mk i))
α : Type u
β : Type v
γ : Type ?u.527967
δ : Type ?u.527970
ε : Type ?u.527973
ζ : Type ?u.527976
ι : Type u_1
κ : Type ?u.527982
σ : ι → Type u_2
τ : κ → Type ?u.527992
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), Sigma.fst ⁻¹' {i})
simp only [← range_sigmaMk]
no goals
α : Type u
β : Type v
γ : Type ?u.527967
δ : Type ?u.527970
ε : Type ?u.527973
ζ : Type ?u.527976
ι : Type u_1
κ : Type ?u.527982
σ : ι → Type u_2
τ : κ → Type ?u.527992
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set ι
⊢ IsOpen (⋃ (i : ι) (_ : i ∈ s), range (Sigma.mk i))
exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk