continuousAt — Mathlib

English

An open partial homeomorphism is continuous at every point of its source.

Русский

Открытый частичный гомеоморфизм непрерывен во всех точках своей области определения.

LaTeX

$$$\\forall x \\in \\mathrm{source}(e): \\mathrm{ContinuousAt}(e, x)$$$

Lean4

/-- An open partial homeomorphism is continuous at any point of its source -/
protected theorem continuousAt {x : X} (h : x ∈ e.source) : ContinuousAt e x :=
  (e.continuousOn x h).continuousAt (e.open_source.mem_nhds h)

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