instDiscrete_unitLattice — Mathlib

English

The unit lattice inside the real-analytic framework is discrete, i.e., the topology is that of a discrete lattice on the units modulo torsion.

Русский

Единичная решетка внутри аналитического контекста дискретна, топология соответствует дискретной решётке на единицах по модулю torsion.

LaTeX

$$$\text{IsZLattice}(\mathbb{R}, \mathrm{unitLattice}(K))$$$

Lean4

instance instDiscrete_unitLattice : DiscreteTopology (unitLattice K) := by
  classical
  refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩

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