continuous_setToFun — Mathlib

English

The map sending f to setToFun μ T hT f is continuous on the space of L1-functions.

Русский

Карту, отправляющую f в setToFun μ T hT f, можно рассматривать как непрерывную на пространстве L1-функций.

LaTeX

$$$\text{continuous}_{f:\alpha\to E} (\mathrm{setToFun}(\mu, T) h_T f)$$$

Lean4

@[continuity]
theorem continuous_setToFun (hT : DominatedFinMeasAdditive μ T C) : Continuous fun f : α →₁[μ] E => setToFun μ T hT f :=
  by simp_rw [L1.setToFun_eq_setToL1 hT]; exact ContinuousLinearMap.continuous _

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