cauchy_inf_uniformSpace — Mathlib

English

A filter is Cauchy for the infimum of two uniformities iff it is Cauchy for each of them.

Русский

Фильтр является Коши для наименьшей (пересечения) двух равномерностей тогда и только тогда, когда он Коши для каждой из них.

LaTeX

$$$ \text{Cauchy}(F) \iff \text{Cauchy}(F)\text{(uniformity } u) \wedge \text{Cauchy}(F)\text{(uniformity } v)$ при инфимум-равномерности $u \sqcap v$$$

Lean4

theorem cauchy_inf_uniformSpace {u v : UniformSpace β} {F : Filter β} :
    Cauchy (uniformSpace := u ⊓ v) F ↔ Cauchy (uniformSpace := u) F ∧ Cauchy (uniformSpace := v) F :=
  by
  unfold Cauchy
  rw [inf_uniformity (u := u), le_inf_iff, and_and_left]

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