continuous_inf_dom_right

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#continuous_inf_dom_right

← MathLib Explorer

English

If f is continuous, then f is continuous from α ⊓ t2 to t3.

Русский

Если f непрерывна, то она непрерывна от α ⊓ t2 к t3.

LaTeX

$$$$ \text{Continuous} f \Rightarrow \text{Continuous}[t_1 \wedge t_2, t_3] f. $$$$

Lean4

theorem continuous_inf_dom_right {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₂, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f :=
  continuous_le_dom inf_le_right

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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