isometry_restrict — Mathlib

English

The map F(s) = UniformFun.ofFun ∘ s.restrict ∘ toFun { s } is an isometry from (α →ᵤ[{ s }] β) to (s →ᵤ β).

Русский

Отображение F = UniformFun.ofFun ∘ s.restrict ∘ toFun { s } является изометрией между (α →ᵤ[{ s }] β) и (s →ᵤ β).

LaTeX

$$$\mathrm{Isometry}\big( \mathrm{UniformFun.ofFun} \circ s.restrict \circ \mathrm{toFun} \{ s \} \big)$$$

Lean4

theorem isometry_restrict (s : Set α) :
    Isometry (UniformFun.ofFun ∘ s.restrict ∘ toFun { s } : (α →ᵤ[{ s }] β) → (s →ᵤ β)) := by
  simp [Isometry, edist_def, UniformFun.edist_def, iSup_subtype]

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