α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ IsClosed (Sigma.mk i '' s)
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
⊢ IsClosedMap (Sigma.mk i)
intro s hs
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ ∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ IsClosed (Sigma.mk i '' s)
rw [isClosed_sigma_iff]
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
⊢ ∀ (i_1 : ι), IsClosed (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))
intro j
case inl
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsClosed s
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

case inr
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
⊢ IsClosed (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.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
j : ι
s : Set (σ j)
hs : IsClosed s
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk j '' s))
rwa [Set.preimage_image_eq _ sigma_mk_injective]
case inr
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed ∅
case inr
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
rw [preimage_image_sigmaMk_of_ne hne]
no goals
case inr
α : Type u
β : Type v
γ : Type ?u.515690
δ : Type ?u.515693
ε : Type ?u.515696
ζ : Type ?u.515699
ι : Type u_2
κ : Type ?u.515705
σ : ι → Type u_1
τ : κ → Type ?u.515715
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
i : ι
s : Set (σ i)
hs : IsClosed s
j : ι
hne : j ≠ i
⊢ IsClosed ∅
exact isClosed_empty