English
For finite index set, the distance between the pointwise infimum and supremum equals the distance between the two vectors, i.e., dist(x ⊓ y, x ⊔ y) = dist(x, y).
Русский
Для конечного множества индексов расстояние между точечными инфимумом и супремумом равно расстоянию между векторами: dist(x ⊓ y, x ⊔ y) = dist(x, y).
LaTeX
$$$\operatorname{dist}(x \wedge y, x \vee y) = \operatorname{dist}(x, y)$$$
Lean4
theorem mem_interior_of_forall_lt (hs : IsUpperSet s) (hx : x ∈ closure s) (h : ∀ i, x i < y 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, z i < y i :=
by
refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.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 ((lt_sub_iff_add_lt.2 <| hyz _).trans (hw _ <| mem_univ _).1).le
