mono_uniformSpace — Mathlib

English

If u ≤ v are uniform structures on β and F is Cauchy with respect to u, then F is Cauchy with respect to v.

Русский

Если u ≤ v — равномерные структуры на β и фильтр F является Коши по отношению к u, то он Коши и по отношению к v.

LaTeX

$$$ u \le v \rightarrow \text{Cauchy}(F)\text{ (uniformity } u) \rightarrow \text{Cauchy}(F)\text{ (uniformity } v)$$$

Lean4

theorem mono_uniformSpace {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v) (hF : Cauchy (uniformSpace := u) F) :
    Cauchy (uniformSpace := v) F :=
  ⟨hF.1, hF.2.trans huv⟩

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