English
For a closed S in X, under T1 and WeaklyLocallyCompact assumptions, Tendsto Subtype.val cofinite (cocompact X) holds iff S is discrete as a subspace.
Русский
Для замкнутого S в X при T1 и слабой локальной локальности выполняется эквивалентность: Tendsto Subtype.val cofinite (cocompact X) ⇔ DiscreteTopology S.
LaTeX
$$$\\mathrm{Tendsto}\\ \\mathrm{Subtype.val} \\operatorname{cofinite} (\\operatorname{cocompact} X) \\iff \\text{DiscreteTopology } S$$$
Lean4
theorem tendsto_coe_cofinite_iff [T1Space X] [WeaklyLocallyCompactSpace X] {s : Set X} (hs : IsClosed s) :
Tendsto ((↑) : s → X) cofinite (cocompact _) ↔ DiscreteTopology s :=
⟨continuous_subtype_val.discrete_of_tendsto_cofinite_cocompact, fun _ ↦
hs.tendsto_coe_cofinite_of_discreteTopology inferInstance⟩
