cocompact_inf_nhds_neBot — Mathlib

English

For any p, the infimum cocompact on ℚ and the neighborhood filter at p is nontrivial.

Русский

Для любого p плотность инфиминтивного кокомпакта на ℚ и фильтра окрестностей в p не тривиальны.

LaTeX

$$$\operatorname{NeBot}(\operatorname{cocompact}\mathbb{Q} \sqcap \mathcal{N}(p))$$$

Lean4

instance cocompact_inf_nhds_neBot : NeBot (cocompact ℚ ⊓ 𝓝 p) :=
  by
  refine (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 ?_
  rintro ⟨s, o⟩ ⟨hs, hpo, ho⟩; rw [inter_comm]
  exact (dense_compl_compact hs).inter_open_nonempty _ ho ⟨p, hpo⟩

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