norm_restrict_mono_set — Mathlib

English

Another instance of monotonicity of restriction norms with respect to compact inclusions.

Русский

Еще одно повторение монотонности норм ограничений по включениям компактов.

LaTeX

$$$\|f.restrict K\| \le \|f.restrict L\|$$$

Lean4

theorem norm_restrict_mono_set {X : Type*} [TopologicalSpace X] (f : C(X, E)) {K L : TopologicalSpace.Compacts X}
    (hKL : K ≤ L) : ‖f.restrict K‖ ≤ ‖f.restrict L‖ :=
  (norm_le _ (norm_nonneg _)).mpr fun x => norm_coe_le_norm (f.restrict L) <| Set.inclusion hKL x

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