English
A set is open iff every point has a positive radius such that a dist-ball around it stays inside.
Русский
Множество открыто, если для каждой точки существует положительный радиус, чтобы шар по расстоянию оставался внутри.
LaTeX
$$$$ IsOpen(s) \iff \forall x\in s, \exists \varepsilon>0, \forall y, \operatorname{dist}(x,y) < \varepsilon \Rightarrow y \in s $$$$
Lean4
theorem isOpen_iff_dist (s : Set (∀ n, E n)) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s :=
by
constructor
· intro hs x hx
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
rw [← mem_cylinder_iff_eq.1 h'x] at h's
exact ⟨(1 / 2 : ℝ) ^ n, by simp, fun y hy => h's fun i hi => (apply_eq_of_dist_lt hy hi.le).symm⟩
· intro h
refine (isTopologicalBasis_cylinders E).isOpen_iff.2 fun x hx => ?_
rcases h x hx with ⟨ε, εpos, hε⟩
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos one_half_lt_one
refine ⟨cylinder x n, ⟨x, n, rfl⟩, self_mem_cylinder x n, fun y hy => hε y ?_⟩
rw [PiNat.dist_comm]
exact (mem_cylinder_iff_dist_le.1 hy).trans_lt hn
