Distance_from_Subset_of_Real_Numbers
Provedanalysismetric-spacesproofwiki
For any non-empty subset S of reals and any real x, the distance from x to S is non-negative and well-defined.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Distance_from_Subset_of_Real_Numbers (S : Set ℝ) (hS : S.Nonempty) (x : ℝ) : ∃ d : ℝ, d = iInf (fun s : S => |x - (s : ℝ)|) ∧ 0 ≤ d := by sorry
Source