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