α : Type u
β : Type v
γ : Type ?u.514064
δ : Type ?u.514067
ε : Type ?u.514070
ζ : Type ?u.514073
ι : Type u_2
κ : Type ?u.514079
σ : ι → Type u_1
τ : κ → Type ?u.514089
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
α : Type u
β : Type v
γ : Type ?u.514064
δ : Type ?u.514067
ε : Type ?u.514070
ζ : Type ?u.514073
ι : Type u_2
κ : Type ?u.514079
σ : ι → Type u_1
τ : κ → Type ?u.514089
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
delta instTopologicalSpaceSigma
α : Type u
β : Type v
γ : Type ?u.514064
δ : Type ?u.514067
ε : Type ?u.514070
ζ : Type ?u.514073
ι : Type u_2
κ : Type ?u.514079
σ : ι → Type u_1
τ : κ → Type ?u.514089
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
α : Type u
β : Type v
γ : Type ?u.514064
δ : Type ?u.514067
ε : Type ?u.514070
ζ : Type ?u.514073
ι : Type u_2
κ : Type ?u.514079
σ : ι → Type u_1
τ : κ → Type ?u.514089
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
rw [isOpen_iSup_iff]
no goals
α : Type u
β : Type v
γ : Type ?u.514064
δ : Type ?u.514067
ε : Type ?u.514070
ζ : Type ?u.514073
ι : Type u_2
κ : Type ?u.514079
σ : ι → Type u_1
τ : κ → Type ?u.514089
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
s : Set (Sigma σ)
⊢ (∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
rfl