continuous_bot — Mathlib

English

For any map f: α → β, the function is continuous from the bottom topology ⊥ on α to any topology t on β.

Русский

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

LaTeX

$$$\\forall f: \\alpha \\to \\beta,\\; \\text{Continuous}[\\perp, t]\, f.$$$

Lean4

@[continuity, fun_prop]
theorem continuous_bot {t : TopologicalSpace β} : Continuous[⊥, t] f :=
  continuous_iff_le_induced.2 bot_le

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