instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples

English

The coercion from integers to reals tends to cocompact with respect to the cofinite filter.

Русский

Отображение целых чисел в действительные стремится к коккомпактности относительно фильтра cofinite.

LaTeX

$$$\\operatorname{Tendsto}(\\uparrow: \\mathbb{Z} \\to \\mathbb{R})\\;\\mathrm{cofinite}\\; (\\mathrm{cocompact}\\ \\mathbb{R})$$$

Lean4

/-- This is a special case of `NormedSpace.discreteTopology_zmultiples`. It exists only to simplify
dependencies. -/
instance {a : ℝ} : DiscreteTopology (AddSubgroup.zmultiples a) :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))
  rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
  refine ⟨ball 0 |a|, isOpen_ball, ?_⟩
  ext ⟨x, hx⟩
  obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
  simp [ha, Real.dist_eq, abs_mul, (by norm_cast : |(k : ℝ)| < 1 ↔ |k| < 1)]

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