nndist_eq — Mathlib

English

The nonnegative distance between f and g equals the infimum of all C such that ∀ x, nndist(f x, g x) ≤ C.

Русский

Непрерывное неотрицательное расстояние между f и g равно инфимума всех C, удовлетворяющих ∀ x, nndist(f x, g x) ≤ C.

LaTeX

$$dist_eq : nndist f g = sInf {C | ∀ x : α, nndist (f x) (g x) ≤ C}$$

Lean4

theorem nndist_eq : nndist f g = sInf {C | ∀ x : α, nndist (f x) (g x) ≤ C} :=
  Subtype.ext <|
    dist_eq.trans <| by
      rw [val_eq_coe, coe_sInf, coe_image]
      simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]

Похожие утверждения