instNormOneClass — Mathlib

English

If the unit in β has norm one and α is nonempty, then the constant function 1 in α →ᵇ β has norm 1.

Русский

Пусть единица β имеет норму 1 и α непусто; тогда константная функция 1 в α →ᵇ β имеет норму 1.

LaTeX

$$$\|\mathbf{1}\| = 1$ in $\alpha \to^b \beta$ (when $α\neq\varnothing$, $‖1_{β}‖=1$).$$

Lean4

/-- If `‖(1 : β)‖ = 1`, then `‖(1 : α →ᵇ β)‖ = 1` if `α` is nonempty. -/
instance instNormOneClass [Nonempty α] [One β] [NormOneClass β] : NormOneClass (α →ᵇ β) where
  norm_one := by simp only [norm_eq_iSup_norm, coe_one, Pi.one_apply, norm_one, ciSup_const]

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