English
For a closed set s that is nonempty, and x ∉ s, there exists n with s and cylinder(x,n) disjoint.
Русский
Для замкнутого непустого множества s и точки x ∉ s существует n такое, что s и цилиндр(x,n) не пересекаются.
LaTeX
$$$$ \exists n, \; \mathrm{Disjoint}(s, \mathrm{cylinder}(x,n)) $$$$
Lean4
theorem exists_disjoint_cylinder {s : Set (∀ n, E n)} (hs : IsClosed s) {x : ∀ n, E n} (hx : x ∉ s) :
∃ n, Disjoint s (cylinder x n) :=
by
rcases eq_empty_or_nonempty s with (rfl | hne)
· exact ⟨0, by simp⟩
have A : 0 < infDist x s := (hs.notMem_iff_infDist_pos hne).1 hx
obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < infDist x s := exists_pow_lt_of_lt_one A one_half_lt_one
refine ⟨n, disjoint_left.2 fun y ys hy => ?_⟩
apply lt_irrefl (infDist x s)
calc
infDist x s ≤ dist x y := infDist_le_dist_of_mem ys
_ ≤ (1 / 2) ^ n := by
rw [mem_cylinder_comm] at hy
exact mem_cylinder_iff_dist_le.1 hy
_ < infDist x s := hn
