case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s → ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ (∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen s
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s ↔ ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
constructor
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen s → ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
intro hs x hx
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder y n ⊆ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
obtain ⟨v, ⟨y, n, rfl⟩, h'x, h's⟩ :
    ∃ v ∈ { s | ∃ (x : ∀ n : ℕ, E n) (n : ℕ), s = cylinder x n }, x ∈ v ∧ v ⊆ s :=
  (isTopologicalBasis_cylinders E).exists_subset_of_mem_open hx hs
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder y n ⊆ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
rw [← mem_cylinder_iff_eq.1 h'x] at h's
no goals
case mp.intro.intro.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
exact
  ⟨(1 / 2 : ℝ) ^ n, by simp, fun y hy => h's fun i hi => (apply_eq_of_dist_lt hy hi.le).symm⟩
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen s
x : (n : ℕ) → E n
hx : x ∈ s
y : (n : ℕ) → E n
n : ℕ
h'x : x ∈ cylinder y n
h's : cylinder x n ⊆ s
⊢ (1 / 2) ^ n > 0
simp
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ IsOpen s
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ (∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s) → IsOpen s
intro h
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ IsOpen s
refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_
case mpr.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
case mpr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
rcases h x hx with ⟨ε, εpos, hε⟩
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
case mpr.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist x y < ε
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
⊢ ∃ t, t ∈ {s | ∃ x n, s = cylinder x n} ∧ x ∈ t ∧ t ⊆ s
refine' ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y _⟩
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist y x < ε
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist x y < ε
rw [PiNat.dist_comm]
no goals
case mpr.intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
h : ∀ (x : (n : ℕ) → E n), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
x : (n : ℕ) → E n
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
n : ℕ
hn : (1 / 2) ^ n < ε
y : (n : ℕ) → E n
hy : y ∈ cylinder x n
⊢ dist y x < ε
exact (mem_cylinder_iff_dist_le.1 hy).trans_lt hn