cauchy_iInf_uniformSpace — Mathlib

English

Let ι be nonempty and u_i be a family of uniform structures. A filter is Cauchy with respect to the infimum uniformity ⨅ i, u_i iff it is Cauchy with respect to every u_i.

Русский

Пусть ι непусто; семейство равномерностей {u_i}. Фильтр является Коши для инф-равномерности ⨅ i, u_i тогда и только тогда, когда он является Коши для каждого u_i.

LaTeX

$$$ \text{Cauchy}(F) \iff \forall i,\; \text{Cauchy}(F)\text{(uniformity } u_i)$ при $u = \bigwedge_i u_i$$$

Lean4

theorem cauchy_iInf_uniformSpace {ι : Sort*} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β} :
    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l :=
  by
  unfold Cauchy
  rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

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