comp'

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#Continuous.comp'

English

If f is continuous, then every iterate f^[n] is continuous.

Русский

Если f непрерывна, то каждая итерация f^[n] непрерывна.

LaTeX

$$$\\mathrm{Continuous}(f) \\Rightarrow \\forall n \\in \\mathbb{N}, \\mathrm{Continuous}(f^{\\circ n})$$$

Lean4

@[continuity, fun_prop]
theorem comp' {g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous (fun x => g (f x)) :=
  hg.comp hf

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

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

Разделы

Аффилиация

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