tendsto_coe_cofinite_of_discreteTopology

English

If s is a closed subset of X and s carries the discrete topology, then the inclusion map s → X tends to cocompact X in the cocompact topology.

Русский

Если s — замкнутое подмножество X и s имеет дискретную топологию, то вложение s → X стремится к cocompact в X.

LaTeX

$$$\\operatorname{Tendsto} (\\text{Subtype.val})\\cofinite(\\operatorname{cocompact} _) $$$

Lean4

theorem tendsto_coe_cofinite_of_discreteTopology {s : Set X} (hs : IsClosed s) (_hs' : DiscreteTopology s) :
    Tendsto ((↑) : s → X) cofinite (cocompact _) :=
  tendsto_cofinite_cocompact_of_discrete hs.isClosedEmbedding_subtypeVal.tendsto_cocompact

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