The current definition of Subnet requires (certain forms of) functional extensionality even for simple facts like "every net is a subnet of itself". By restating the definition in an extensional way, such problems/axioms can be avoided.
Also, this PR changes DS_set to be a coercion DirectedSet >-> Sortclass, to simplify various terms. This is analogous to the existing coercion point_set : TopologicalSpace >-> Sortclass.
The current definition of
Subnetrequires (certain forms of) functional extensionality even for simple facts like "every net is a subnet of itself". By restating the definition in an extensional way, such problems/axioms can be avoided.Also, this PR changes
DS_setto be a coercionDirectedSet >-> Sortclass, to simplify various terms. This is analogous to the existing coercionpoint_set : TopologicalSpace >-> Sortclass.