Showing changes from revision #1 to #2:
Added | Removed | Changed
Let be the Dedekind real numbers with a term
representing that the shape of is contractible ( (which derives fromaxiom R0?axiom R-flat), and let be a closed interval or open interval in . Because the shape of is contractible, the shape of any closed or open interval in is contractible. Given a mapping , let us define the graph of the mapping as
in the product type . is continuous if the shape of is contractible:
Let and be space?s with terms
representing that the shapes of and are contractible. Given a mapping , let us define the graph of the mapping as
in the product type . is continuous if the shape of is contractible: