English
Let f: α → E tend to the unit element 1 along a filter l, and let g: α → F be bounded in norm along l. For a binary operation op: E × F → G satisfying ∥op x y∥ ≤ ∥x∥∥y∥, the function x ↦ op(f(x), g(x)) tends to 1 along l.
Русский
Пусть f: α → E стремится к единице вдоль фильтра l, и пусть g: α → F ограничен по норме вдоль l. При бинарной операции op: E × F → G с неравенством ∥op x y∥ ≤ ∥x∥∥y∥, функция x ↦ op(f(x), g(x)) стремится к 1 вдоль l.
LaTeX
$$$\operatorname{Tendsto}\bigl(x \mapsto \operatorname{op}\bigl(f(x), g(x)\bigr)\bigr)\;l\; (\mathcal{N}(1))$$$
Lean4
/-- A helper lemma used to prove that the (scalar or usual) product of a function that tends to one
and a bounded function tends to one. This lemma is formulated for any binary operation
`op : E → F → G` with an estimate `‖op x y‖ ≤ ‖x‖ * ‖y‖` instead of multiplication so that it
can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`. -/
@[to_additive /-- A helper lemma used to prove that the (scalar or usual) product of a function that
tends to zero and a bounded function tends to zero. This lemma is formulated for any binary
operation `op : E → F → G` with an estimate `‖op x y‖ ≤ ‖x‖ * ‖y‖` instead of multiplication so
that it can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`. -/
]
theorem op_one_isBoundedUnder_le {f : α → E} {g : α → F} {l : Filter α} (hf : Tendsto f l (𝓝 1))
(hg : IsBoundedUnder (· ≤ ·) l (Norm.norm ∘ g)) (op : E → F → G) (h_op : ∀ x y, ‖op x y‖ ≤ ‖x‖ * ‖y‖) :
Tendsto (fun x => op (f x) (g x)) l (𝓝 1) :=
hf.op_one_isBoundedUnder_le' hg op ⟨1, fun x y => (one_mul ‖x‖).symm ▸ h_op x y⟩
