Theorem Filter.Tendsto.coprod_of_prod_top_left

Modification history

2025-11-05 14:53
Mathlib/Order/Filter/Prod.lean
feat(Analysis/Normed/Algebra/GelfandMazur): new file (#29649) …
Added Filter.Tendsto.coprod_of_prod_top_leftView on Github →