English
If l is an approximate unit and l' ≤ l with l'.NeBot, then l' is also an approximate unit.
Русский
Если l является аппроксимационной единицей и l' ≤ l, причём l' не тривиален, то и l' является аппроксимационной единицей.
LaTeX
$$$$ \mathrm{IsApproximateUnit}(l) \wedge l' \le l \wedge l'.\mathrmNeBot \Rightarrow \mathrm{IsApproximateUnit}(l'). $$$$
Lean4
/-- If `l` is an approximate unit and `⊥ < l' ≤ l`, then `l'` is also an approximate unit. -/
theorem mono {l l' : Filter α} (hl : l.IsApproximateUnit) (hle : l' ≤ l) [hl' : l'.NeBot] : l'.IsApproximateUnit
where
tendsto_mul_left m := hl.tendsto_mul_left m |>.mono_left hle
tendsto_mul_right m := hl.tendsto_mul_right m |>.mono_left hle
