cauchy_iInf_uniformSpace' — Mathlib

English

A variant stating the equivalence with iInf under NeBot condition.

Русский

Вариант, утверждающий эквивалентность относительно iInf при условии NeBot.

LaTeX

$$$ {l:\text{Filter }\beta} [l.NeBot] :\; Cauchy (uniformSpace := ⨅ i, u_i) l \iff \forall i, Cauchy l$$$

Lean4

theorem cauchy_iInf_uniformSpace' {ι : Sort*} {u : ι → UniformSpace β} {l : Filter β} [l.NeBot] :
    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by
  simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]

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