isCoboundedUnder_flip — Mathlib

English

If a filter f is bounded under r, then it is coboundedUnder (flip r) under the same conditions.

Русский

Если фильтр f ограничен по отношению r, то он coboundedUnder (flip r) при тех же условиях.

LaTeX

$$$\forall {f} {u}, [IsTrans α r] [NeBot f] (h : f.IsBoundedUnder r u) : f.IsCoboundedUnder (flip r) u.$$$

Lean4

theorem isCoboundedUnder_flip {u : γ → α} {l : Filter γ} [IsTrans α r] [NeBot l] (h : l.IsBoundedUnder r u) :
    l.IsCoboundedUnder (flip r) u :=
  h.isCobounded_flip

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