continuous_coinduced_dom — Mathlib

English

For g: β → γ, t₁ on α and t₂ on γ, we have Continuous[coinduced f t₁, t₂] g iff Continuous[t₁, t₂] (g ∘ f).

Русский

Для g: β → γ, t₁ на α и t₂ на γ имеют место эквивалентности Continuous[coinduced f t₁, t₂] g ⇔ Continuous[t₁, t₂] (g ∘ f).

LaTeX

$$$$ \text{Continuous}[\mathrm{coinduced}(f,t_1),t_2]\ g \iff \text{Continuous}[t_1,t_2](g \circ f). $$$$

Lean4

theorem continuous_coinduced_dom {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
    Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f) := by
  simp only [continuous_iff_coinduced_le, coinduced_compose]

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