Continuous open maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines bundled continuous open maps.
We use the
fun_like design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
The type of continuous open maps from
β, aka Priestley homomorphisms.
continuous_open_map_class F α β states that
F is a type of continuous open maps.
You should extend this class when you extend
Instances of this typeclass
Instances of other typeclasses for
Helper instance for when there's too many metavariables to apply