mono — Mathlib

English

If f and g are filters with g ≤ f and f is Cauchy, then g is also Cauchy (assuming g is nontrivial).

Русский

Если фильтры f и g удовлетворяют g ≤ f и f является Коши, то и g является Коши (при условии непустоты g).

LaTeX

$$$ Cauchy(f) \rightarrow g \le f \rightarrow Cauchy(g) $ (при условии классового границы)$$

Lean4

theorem mono {f g : Filter α} [hg : NeBot g] (h_c : Cauchy f) (h_le : g ≤ f) : Cauchy g :=
  ⟨hg, le_trans (Filter.prod_mono h_le h_le) h_c.right⟩

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