Theorem RestrictedProduct.continuous_dom_pi

Modification history

2025-09-19 07:04
Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean
chore(*): drop some `Decidable`/`Fintype` assumptions (#29785) …
Modified RestrictedProduct.continuous_dom_piView 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.continuous_dom_piView on Github →