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]