mem_uniformity' — Mathlib

English

If 𝓤(α) has a basis (p,s), then 𝓤(CauchyFilter α) has basis p ∘ gen, via monotone_gen.

Русский

Если у 𝓤(α) есть база (p,s), то у 𝓤(CauchyFilter α) база p ∘ gen через монотонность_gen.

LaTeX

$$$\\text{basis_uniformity}\\;\\Rightarrow\\; (\\mathcal{U}(\\mathrm{CauchyFilter}(\\alpha))).\\text{HasBasis } p (\\mathrm{gen}\\circ s)$$$

Lean4

theorem mem_uniformity' {s : Set (CauchyFilter α × CauchyFilter α)} :
    s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ f g : CauchyFilter α, t ∈ f.1 ×ˢ g.1 → (f, g) ∈ s :=
  by
  refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
  exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩

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