English
For g: γ → α, t₂ on β and t₁ on γ, the map g is continuous from (γ, t₁) to (β, induced f t₂) iff the composition f ∘ g is continuous from (γ, t₁) to (β, t₂).
Русский
Для g: γ → α, t₂ на β и t₁ на γ отображение g непрерывно из (γ, t₁) в (β, induced f t₂) тогда и только тогда, когда композиция f ∘ g непрерывна из (γ, t₁) в (β, t₂).
LaTeX
$$$$ \text{Continuous}[\mathrm{induced}(f,t_2)]\ g \iff \text{Continuous}[t_1,t_2](f \circ g). $$$$
Lean4
theorem continuous_induced_rng {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g) := by
simp only [continuous_iff_le_induced, induced_compose]
