isUniformInducing_pureCauchy — Mathlib

English

The map pureCauchy: α → CauchyFilter α is uniform inducing.

Русский

Функция pureCauchy: α → CauchyFilter α является равномерно индуцирующей.

LaTeX

$$$\\text{IsUniformInducing}(\\text{pureCauchy} : \\alpha \\to \\mathrm{CauchyFilter}(\\alpha))$$$

Lean4

theorem isUniformInducing_pureCauchy : IsUniformInducing (pureCauchy : α → CauchyFilter α) :=
  ⟨have : (preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen = id :=
      funext fun s => Set.ext fun ⟨a₁, a₂⟩ => by simp [preimage, gen, pureCauchy]
    calc
      comap (fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ((𝓤 α).lift' gen) =
          (𝓤 α).lift' ((preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) :=
        comap_lift'_eq
      _ = 𝓤 α := by simp [this]⟩

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