isUniformInducing_iff — Mathlib

English

If f is IsUniformInducing, then Cauchy (map f F) is equivalent to Cauchy F for any filter F.

Русский

Если f является равномерно индуцирующим, то Cauchy (map f F) эквивалентно Cauchy F для любого фильтра.

LaTeX

$$$\\text{Cauchy }(\\text{map } f F) \\iff \\text{Cauchy }F$$$

Lean4

protected theorem isUniformInducing_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s)
    (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
    IsUniformInducing f ↔
      (∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) :=
  by simp [isUniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]

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