continuous_top — Mathlib

English

For any f: α → β, the map is continuous from any topology t on α to the top (discrete) topology on β.

Русский

Для любой функции f: α → β отображение непрерывно при некоторой топологии t на α к дискретной топологии на β.

LaTeX

$$$\\forall t,\\; \\text{Continuous}[t, \\top] f.$$$

Lean4

@[continuity, fun_prop]
theorem continuous_top {t : TopologicalSpace α} : Continuous[t, ⊤] f :=
  continuous_iff_coinduced_le.2 le_top

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