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]