tendsto_cofinite_cocompact_of_discrete

English

If X is discrete, Tendsto f (cocompact X) (cocompact Y) implies Tendsto f cofinite (cocompact Y).

Русский

Если X дискретно, Tendsto f (cocompact X) (cocompact Y) следует из Tendsto f cofinite (cocompact Y).

LaTeX

$$$\\mathrm{Tendsto}\\ f\\ (\\mathrm{cocompact}\\ X)\\ (\\mathrm{cocompact}\\ Y) \\Rightarrow \\mathrm{Tendsto}\\ f\\ \\mathrm{cofinite}\\ (\\mathrm{cocompact}\\ Y)$$$

Lean4

theorem tendsto_cofinite_cocompact_of_discrete [DiscreteTopology X] (hf : Tendsto f (cocompact _) (cocompact _)) :
    Tendsto f cofinite (cocompact _) := by
  convert hf
  rw [cocompact_eq_cofinite X]

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