continuousOn — Mathlib

English

Let e be an OpenPartialHomeomorph X Y. Then the restriction of e to its source is continuous on that domain: ContinuousOn e e.source.

Русский

Пусть e—открыто-частичный гомеоморфизм X → Y. Тогда ограничение e на область определения e.source непрерывно на этой области: ContinuousOn e e.source.

LaTeX

$$$\mathrm{ContinuousOn}(e, e.source).$$$

Lean4

protected theorem continuousOn : ContinuousOn e e.source :=
  e.continuousOn_toFun

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