continuous_empty_function — Mathlib

English

If β is empty, any function f: α → β is continuous.

Русский

Если целевое пространство пусто, любое отображение непрерывно.

LaTeX

$$$[\text{IsEmpty } \beta] \Rightarrow \operatorname{Continuous}(f)$$$

Lean4

/-- See also `continuous_of_discreteTopology`, which works for `IsEmpty α`. -/
theorem continuous_empty_function [TopologicalSpace α] [TopologicalSpace β] [IsEmpty β] (f : α → β) : Continuous f :=
  letI := Function.isEmpty f
  continuous_of_discreteTopology

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