English
For a finite index set, the lower closure of the interior of s is contained in the interior of the lower closure of s.
Русский
Для конечного множества индексов нижнее замыкание Interior s содержится в Interior нижнего замыкания s.
LaTeX
$$$\operatorname{lowerClosure}(\operatorname{interior}s) \subseteq \operatorname{interior}(\operatorname{lowerClosure}s)$$$
Lean4
theorem exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s) (hδ : 0 < δ) :
∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s :=
by
refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
· rw [dist_self_sub_left]
refine (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq ?_
simp only [norm_mul, norm_div, Real.norm_eq_abs, zero_lt_three, abs_of_pos, zero_lt_four, abs_of_pos hδ]
ring
obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
rw [mem_closedBall, dist_eq_norm'] at hz
rw [dist_eq_norm] at hxy
replace hxy := (norm_le_pi_norm _ i).trans hxy.le
replace hz := (norm_le_pi_norm _ i).trans hz
dsimp at hxy hz
rw [abs_sub_le_iff] at hxy hz
linarith
