edist_def' — Mathlib

English

For finite 𝔖, edist f g equals the iterated supremum over s ∈ 𝔖 of the supremum over x ∈ s of edist (toFun 𝔖 f x) (toFun 𝔖 g x).

Русский

Для конечного 𝔖 edist f g равно по сути двойной супремум над s ∈ 𝔖 и над x ∈ s.

LaTeX

$$$edist f g = \bigsqcup_{s \in 𝔖} \bigsqcup_{x \in s} edist (toFun 𝔖 f x) (toFun 𝔖 g x)$$$

Lean4

theorem edist_def' [Finite 𝔖] (f g : α →ᵤ[𝔖] β) : edist f g = ⨆ s ∈ 𝔖, ⨆ x ∈ s, edist (toFun 𝔖 f x) (toFun 𝔖 g x) := by
  simp [edist_def, iSup_and, iSup_comm (ι := α)]

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