English
A bornology on a set can be generated from a distance function satisfying symmetry and triangle inequality in a bounded sense.
Русский
Барогология на множестве строится из функции расстояния, удовлетворяющей симметрии и треугольному неравенству в ограниченном смысле.
LaTeX
$$$\text{Bornology}(\alpha)$ задана как множество ограниченных подмножеств, порождённое через dist.$$
Lean4
/-- Construct a bornology from a distance function and metric space axioms. -/
abbrev ofDist {α : Type*} (dist : α → α → ℝ) (dist_comm : ∀ x y, dist x y = dist y x)
(dist_triangle : ∀ x y z, dist x z ≤ dist x y + dist y z) : Bornology α :=
Bornology.ofBounded {s : Set α | ∃ C, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C} ⟨0, fun _ hx _ => hx.elim⟩
(fun _ ⟨c, hc⟩ _ h => ⟨c, fun _ hx _ hy => hc (h hx) (h hy)⟩)
(fun s hs t ht => by
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
· rwa [empty_union]
rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
· rwa [union_empty]
rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
· refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)
rcases hs with ⟨Cs, hs⟩; rcases ht with ⟨Ct, ht⟩
refine
⟨max Cs (dist x y + Ct), fun z hz =>
hz.elim (fun hz => (hs hx hz).trans (le_max_left _ _))
(fun hz => (dist_triangle x y z).trans <| (add_le_add le_rfl (ht hy hz)).trans (le_max_right _ _))⟩)
fun z => ⟨dist z z, forall_eq.2 <| forall_eq.2 le_rfl⟩
