E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (Set.pi ↑(Finset.range n) fun i => {x i})
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (cylinder x n)
rw [PiNat.cylinder_eq_pi]
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (Set.pi ↑(Finset.range n) fun i => {x i})
exact isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _