THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the
has_continuous_star typeclass, along with instances on
Basic hypothesis to talk about a topological space with a continuous
Instances of this typeclass
The star operation bundled as a continuous map.