mem_entourage — Mathlib

English

If β index set supports a Cauchy sequence u, then β must be nonempty.

Русский

Если существует Коши-последовательность с индексами в β, то β не пусто.

LaTeX

$$$\\text{Nonempty}(\\beta).$$$

Lean4

theorem mem_entourage {β : Type*} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : Set (α × α)} (hV : V ∈ 𝓤 α) :
    ∃ k₀, ∀ i j, k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V :=
  by
  haveI := h.nonempty
  have := h.tendsto_uniformity; rw [← prod_atTop_atTop_eq] at this
  simpa [MapsTo] using atTop_basis.prod_self.tendsto_left_iff.1 this V hV

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