edist_def — Mathlib

English

For finite 𝔖, the edistance between f and g in α →ᵤ[𝔖] β is the supremum over x ∈ ⋃₀ 𝔖 of the distances edist (toFun 𝔖 f x) (toFun 𝔖 g x).

Русский

Для конечного 𝔖 евдистанция edist между f и g в α →ᵤ[𝔖] β равна супремуму по x ∈ ⋃₀ 𝔖 расстояния edist (toFun 𝔖 f x) (toFun 𝔖 g x).

LaTeX

$$$edist f g = \bigvee_{x \in \bigcup_0 𝔖} edist (toFun 𝔖 f x) (toFun 𝔖 g x)$$$

Lean4

theorem edist_def [Finite 𝔖] (f g : α →ᵤ[𝔖] β) : edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist (toFun 𝔖 f x) (toFun 𝔖 g x) :=
  rfl

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