continuous_id_of_le — Mathlib

English

If t ≤ t' for topologies t, t' on α, then the identity map id: (α,t) → (α,t') is continuous.

Русский

Если тождественная карта удовлетворяет t ≤ t' для топологий t, t' на α, то она непрерывна.

LaTeX

$$$t \\le t' \\Rightarrow \\text{Continuous}_{t,t'}(\\mathrm{id}).$$$

Lean4

theorem continuous_id_of_le {t t' : TopologicalSpace α} (h : t ≤ t') : Continuous[t, t'] id :=
  continuous_id_iff_le.2 h

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