English
Infimum distance is preserved by isometries: infEdist (Φ x) (Set.image Φ t) = infEdist x t for isometry Φ.
Русский
Инвариантность infEdist под изометриями: infEdist(Φ x) (Φ'' t) = infEdist x t.
LaTeX
$$$\infEdist(\Phi x) (\operatorname{image}(\Phi) t) = \infEdist x t$$$
Lean4
theorem exists_pos_forall_lt_edist (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :
∃ r : ℝ≥0, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (r : ℝ≥0∞) < edist x y :=
by
rcases s.eq_empty_or_nonempty with (rfl | hne)
· use 1
simp
obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEdist.continuousOn
have : 0 < infEdist x t := pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEdist_zero_of_closed ht).mpr H⟩
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h hy) z hz⟩
