English
If r is transitive and directed, then the supremum of two r-bounded filters f and g is r-bounded provided both f and g are r-bounded individually.
Русский
Если r транзитивно и направлено, то супремуп двух ограниченных r-фильтров f и g сохраняет ограниченность, если оба f и g ограничены отдельно.
LaTeX
$$$$ [IsTrans\; \alpha\; r] [IsDirected\; \alpha\; r] : IsBounded\; r\; f \to IsBounded\; r\; g \to IsBounded\; r\; (f \sqcup g) $$$$
Lean4
theorem isBounded_sup [IsTrans α r] [IsDirected α r] : IsBounded r f → IsBounded r g → IsBounded r (f ⊔ g)
| ⟨b₁, h₁⟩, ⟨b₂, h₂⟩ =>
let ⟨b, rb₁b, rb₂b⟩ := directed_of r b₁ b₂
⟨b, eventually_sup.mpr ⟨h₁.mono fun _ h => _root_.trans h rb₁b, h₂.mono fun _ h => _root_.trans h rb₂b⟩⟩
