continuous_iff

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsInducing.continuous_iff

English

If hg is IsInducing g, then Continuous f ↔ Continuous (g ∘ f).

Русский

Если hg — IsInducing g, то Continuous f эквивалентно Continuous (g ∘ f).

LaTeX

$$$\operatorname{IsInducing}(g) \Rightarrow (\operatorname{Continuous}(f) \iff \operatorname{Continuous}(g \circ f)).$$$

Lean4

theorem continuous_iff (hg : IsInducing g) : Continuous f ↔ Continuous (g ∘ f) := by
  simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]

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

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

Разделы

Аффилиация

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