English
If t₂ ≤ t₃, and f is ContinuousOn f with domain t₁ and target t₂, then f is ContinuousOn f with target t₃.
Русский
Если т₂ ≤ т₃ и f непрерывна с источником т₁ и целью t₂, то f непрерывна с источником т₁ и целью t₃.
LaTeX
$$$t_2 \\le t_3 \\Rightarrow (ContinuousOn f s)_{t_2} \\Rightarrow (ContinuousOn f s)_{t_3}$$$
Lean4
/-- If a function is continuous on a set for some topologies, then it is
continuous on the same set with respect to any coarser topology on the target space. -/
theorem mono_rng {α β : Type*} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) {s : Set α}
{f : α → β} (h₂ : @ContinuousOn α β t₁ t₂ f s) : @ContinuousOn α β t₁ t₃ f s := fun x hx _u hu =>
h₂ x hx <| nhds_mono h₁ hu
