mono — Mathlib

English

If f ≤ g (monotone in filters) and f is cobounded, then g is cobounded with respect to the same relation.

Русский

Если фильтр f меньше g, и f кобундирован относительно r, то и g кобундирован относительно r.

LaTeX

$$$f \le g \Rightarrow (f.IsCobounded\ r) \to (g.IsCobounded\ r).$$$

Lean4

theorem mono (h : f ≤ g) : f.IsCobounded r → g.IsCobounded r
  | ⟨b, hb⟩ => ⟨b, fun a ha => hb a (h ha)⟩

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