Theorem RestrictedProduct.eventually

Modification history

2025-06-10 22:59
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …
Modified RestrictedProduct.eventuallyView on Github →
2025-06-03 12:54
Mathlib/Topology/Algebra/RestrictedProduct.lean
feat(Topology/RestrictedProduct): continuity of maps from finite product of restricted product (#25349) …
Added RestrictedProduct.eventuallyView on Github →