isCobounded_le_of_bot — Mathlib

English

If u is f-bounded above and v is f-cobounded above, then u+v is f-cobounded above.

Русский

Если u ограничен сверху по f, а v кобондированно ограничен сверху, то их сумма ограничена сверху по f.

LaTeX

$$$f.IsBoundedUnder(≤)\ u \land f.IsCoboundedUnder(≤)\ v \Rightarrow f.IsCoboundedUnder(≤)\ (u+v)$$$

Lean4

theorem isCobounded_le_of_bot [LE α] [OrderBot α] {f : Filter α} : f.IsCobounded (· ≤ ·) :=
  ⟨⊥, fun _ _ => bot_le⟩

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