isContinuous — Mathlib

English

If G is locally-faithful and cover-dense and preserves covers (Hp), then G is continuous with respect to J and K.

Русский

Если G локально полон и плотен, и сохраняет покрытия, то G непрерывно относит топологии J и K.

LaTeX

$$$G\text{ is continuous with respect to } J,K.$$$

Lean4

theorem isContinuous [G.IsLocallyFaithful K] (Hp : CoverPreserving J K G) : G.IsContinuous J K :=
  isContinuous_of_coverPreserving (compatiblePreserving K G) Hp

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