setFinite_inter — Mathlib

English

The intersection of a bounded set in E with the Z-span submodule is finite when E is Proper.

Русский

Пересечение ограниченного множества в E с подпроизведением Z-порожденного модуля конечно.

LaTeX

$$$\text{Set.Finite}(s \cap \operatorname{span}_{\mathbb{Z}}(\operatorname{range} b)).$$$

Lean4

theorem setFinite_inter [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.IsBounded s) :
    Set.Finite (s ∩ span ℤ (Set.range b)) :=
  by
  have : DiscreteTopology (span ℤ (Set.range b)) := inferInstance
  refine Metric.finite_isBounded_inter_isClosed hs ?_
  rw [← coe_toAddSubgroup]
  exact AddSubgroup.isClosed_of_discrete

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