English
For all finite index i, the function y ↦ dist(y, x) is antitone on the interval (−∞, y] componentwise, i.e., larger y decreases the distance to x in a coordinatewise sense.
Русский
Для каждого i расстояние до x по координате i уменьшается при увеличении y в компоненте i (антонишное поведение слева).
LaTeX
$$$\text{AntitoneOn } (\mathrm{dist}\, \cdot \; y) \; (\, \mathrm{Iic}\; y)$$$
Lean4
theorem mem_interior_of_forall_lt (hs : IsLowerSet s) (hx : x ∈ closure s) (h : ∀ i, y i < x i) : y ∈ interior s :=
by
cases nonempty_fintype ι
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
rw [dist_pi_lt_iff hε] at hxz
have hyz : ∀ i, y i < z i :=
by
refine fun i => (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)
rw [← Real.norm_eq_abs, ← dist_eq_norm]
exact (hxz _).le
obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
refine mem_interior.2 ⟨ball y δ, ?_, isOpen_ball, mem_ball_self hδ⟩
rintro w hw
refine hs (fun i => ?_) hz
simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw
exact ((hw _ <| mem_univ _).2.trans <| hyz _).le
