α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ IsOpen (Sigma.mk i '' s)
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
⊢ IsOpenMap (Sigma.mk i)
intro s hs
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ IsOpen (Sigma.mk i '' s)
rw [isOpen_sigma_iff]
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
intro j
case inl
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsOpen s
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

case inr
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
rcases eq_or_ne j i with (rfl | hne)
no goals
case inl
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsOpen s
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
rwa [Set.preimage_image_eq _ sigma_mk_injective]
case inr
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen ∅
case inr
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
rw [preimage_image_sigmaMk_of_ne hne]
no goals
case inr
α : Type u
β : Type v
γ : Type ?u.514883
δ : Type ?u.514886
ε : Type ?u.514889
ζ : Type ?u.514892
ι : Type u_2
κ : Type ?u.514898
σ : ι → Type u_1
τ : κ → Type ?u.514908
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen ∅
exact isOpen_empty