case h_open
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (u : Set ((n : ℕ) → E n)), u ∈ {s | ∃ x n, s = cylinder x n} → IsOpen u

case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)),
    a ∈ u → IsOpen u → ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ a ∈ v ∧ v ⊆ u
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ IsTopologicalBasis {s | ∃ x n, s = cylinder x n}
apply isTopologicalBasis_of_open_of_nhds
case h_open.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (cylinder x n)
case h_open
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (u : Set ((n : ℕ) → E n)), u ∈ {s | ∃ x n, s = cylinder x n} → IsOpen u
rintro u ⟨x, n, rfl⟩
no goals
case h_open.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (cylinder x n)
apply isOpen_cylinder
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)),
    a ∈ u → IsOpen u → ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ a ∈ v ∧ v ⊆ u
intro x u hx u_open
case h_nhds.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
obtain ⟨v, ⟨U, F, -, rfl⟩, xU, Uu⟩ :
    ∃ v ∈ { S : Set (∀ i : ℕ, E i) | ∃ (U : ∀ i : ℕ, Set (E i)) (F : Finset ℕ),
      (∀ i : ℕ, i ∈ F → U i ∈ { s : Set (E i) | IsOpen s }) ∧ S = (F : Set ℕ).pi U },
    x ∈ v ∧ v ⊆ u :=
  (isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx
    u_open
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
case h_nhds.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
rcases Finset.bddAbove F with ⟨n, hn⟩
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ cylinder x (n + 1) ⊆ Set.pi (↑F) U
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ ∃ v, v ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ v ∧ v ⊆ u
refine' ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans _ Uu⟩
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
⊢ y ∈ Set.pi (↑F) U
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ cylinder x (n + 1) ⊆ Set.pi (↑F) U
intro y hy
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
⊢ ∀ (i : ℕ), i ∈ F → y i ∈ U i
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
⊢ y ∈ Set.pi (↑F) U
suffices ∀ i : ℕ, i ∈ F → y i ∈ U i by simpa
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
⊢ y i ∈ U i
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
⊢ ∀ (i : ℕ), i ∈ F → y i ∈ U i
intro i hi
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ y i ∈ U i
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
⊢ y i ∈ U i
have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ x i ∈ U i
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ y i ∈ U i
rw [this]
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
xU : ∀ (i : ℕ), i ∈ F → x i ∈ U i
⊢ x i ∈ U i
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
⊢ x i ∈ U i
simp only [Set.mem_pi, Finset.mem_coe] at xU
no goals
case h_nhds.intro.intro.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
i : ℕ
hi : i ∈ F
this : y i = x i
xU : ∀ (i : ℕ), i ∈ F → x i ∈ U i
⊢ x i ∈ U i
exact xU i hi
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ Set.pi (↑F) U
Uu : Set.pi (↑F) U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
y : (n : ℕ) → E n
hy : y ∈ cylinder x (n + 1)
this : ∀ (i : ℕ), i ∈ F → y i ∈ U i
⊢ y ∈ Set.pi (↑F) U
simpa