continuousOn

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#CPolynomialOn.continuousOn

English

The same as above, reinforcing the property for continuous-on on a set.

Русский

Тождественно повторяет свойство непрерывности на множестве.

LaTeX

$$CPolynomialOn 𝕜 f s → ContinuousOn f s$$

Lean4

protected theorem continuousOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : ContinuousOn f s :=
  hf.analyticOnNhd.continuousOn

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

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

Разделы

Аффилиация

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