Theorem Filter.Tendsto.finInit

Modification history

2025-07-11 18:12
Mathlib/Topology/Constructions.lean
chore(Topology): rename pi family from π to X (#26828) …
Modified Filter.Tendsto.finInitView on Github →
2025-03-17 06:31
Mathlib/Topology/Constructions.lean
feat: Fin.init and Fin.tail are continuous (#22550) …
Added Filter.Tendsto.finInitView on Github →