mkContinuousOfExistsBound_apply

Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.mkContinuousOfExistsBound_apply

English

repetition of the continuity from a linear map with bound.

Русский

повторение условия непрерывности линейной карты с ограничением.

LaTeX

$$$\text{Continuous}(f)$ under bounded linear conditions$$

Lean4

@[simp]
theorem mkContinuousOfExistsBound_apply (h : ∃ C, ∀ x, ‖f x‖ ≤ C * ‖x‖) (x : E) :
    f.mkContinuousOfExistsBound h x = f x :=
  rfl

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

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

Разделы

Аффилиация

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