English
Let g be a monotone function with appropriate Tendsto at infinity; then IsBoundedUnder (≤) l (g ∘ f) is equivalent to IsBoundedUnder (≤) l f.
Русский
Пусть g монотонна и имеет соответствующую предельную устойчивость; тогда IsBoundedUnder(≤) l (g ∘ f) эквивалентно IsBoundedUnder(≤) l f.
LaTeX
$$$\operatorname{IsBoundedUnder}(\le, l)(g\circ f) \iff \operatorname{IsBoundedUnder}(\le, l)f$$$
Lean4
/-- Filters are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic `isBoundedDefault` in the statements,
in the form `(hf : f.IsBounded (≥) := by isBoundedDefault)`. -/
@[tactic_parser 1000]
public meta def tacticIsBoundedDefault : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Filter.tacticIsBoundedDefault 1024 (ParserDescr.nonReservedSymbol✝ "isBoundedDefault" false✝)
