continuous_trans

Mathlib.Topology.Path

URI: https://scilib.ai/kg/mathlib#Path.continuous_trans

English

The map (f,g) ↦ t ↦ (f(t)).trans (g(t)) is continuous in the appropriate product topology.

Русский

Карта (f,g) ↦ t ↦ (f(t)).trans(g(t)) непрерывна во входной пары путей.

LaTeX

$$Continuous (λ p, (p.1)).trans (λ p, (p.2))$$

Lean4

@[continuity, fun_prop]
theorem continuous_trans {x y z : X} : Continuous fun ρ : Path x y × Path y z => ρ.1.trans ρ.2 := by fun_prop

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

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

Разделы

Аффилиация

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