tendsto_coe_cofinite_of_discrete — Mathlib

English

If f: H →* G is an injective monoid hom with discrete topology on its range, then Tendsto f cofinite (cocompact G).

Русский

Если f: H →* G инъективно, голомоморфизм моноида, диапазон у которого имеет дискретную топологию, тогда отображение f является кофинитным к кокомпактному фильтру.

LaTeX

$$$[T2Space\ G] \{H: Type*\} [Group H] {f : H \to* G} (hf : Function.Injective f) (hf' : DiscreteTopology f.range) : Tendsto f cofinite (cocompact G).$$$

Lean4

@[to_additive]
theorem tendsto_coe_cofinite_of_discrete [T2Space G] {H : Type*} [Group H] {f : H →* G} (hf : Function.Injective f)
    (hf' : DiscreteTopology f.range) : Tendsto f cofinite (cocompact _) :=
  by
  replace hf : Function.Injective f.rangeRestrict := by simpa
  exact f.range.tendsto_coe_cofinite_of_discrete.comp hf.tendsto_cofinite

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