continuous_inf_dom_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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