instNormedStarGroup

Mathlib.Topology.ContinuousMap.Bounded.Star

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instNormedStarGroup

English

The underlying function of f.nnnorm is given by the composition NNNorm.nnnorm ∘ f.

Русский

Базовая функция f.nnnorm задаётся как композиция NNNorm.nnnorm ∘ f.

LaTeX

$$$$ (nnnorm\ f)^{\wedge} = NNNorm.nnnorm \circ f. $$$$

Lean4

instance instNormedStarGroup : NormedStarGroup (α →ᵇ β) where
  norm_star_le f := by simp only [norm_eq, star_apply, norm_star, le_of_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru