Homotopy Type Theory
continuous mapping > history (Rev #1, changes)
Showing changes from revision #0 to #1:
Added | Removed | Changed
Definition
In real numbers
Let ℝ \mathbb{R} be the Dedekind real numbers with a term
p ℝ : isContr ( esh ( ℝ ) ) p_\mathbb{R}:isContr(\esh(\mathbb{R}))
representing that the shape of ℝ \mathbb{R} is contractible (axiom R0? ), and let I I be a closed interval or open interval in ℝ \mathbb{R} . Because the shape of ℝ \mathbb{R} is contractible, the shape of any closed or open interval in ℝ \mathbb{R} is contractible. Given a mapping f : I → ℝ f:I \to \mathbb{R} , let us define the graph G G of the mapping f f as
G ≔ ∑ x : I ( x , f ( x ) ) G \coloneqq \sum_{x:I} (x, f(x))
in the product type I × ℝ I \times \mathbb{R} . f f is continuous if the shape of G G is contractible:
p : isContr ( esh ( G ) ) p:isContr(\esh(G))
Between geometrically contractible spaces
Let S S and T T be space? s with terms
p S : isContr ( esh ( S ) ) p_S:isContr(\esh(S)) p T : isContr ( esh ( T ) ) p_T:isContr(\esh(T))
representing that the shape s of S S and T T are contractible . Given a mapping f : S → T f:S \to T , let us define the graph G G of the mapping f f as
G ≔ ∑ x : S ( x , f ( x ) ) G \coloneqq \sum_{x:S} (x, f(x))
in the product type I × ℝ I \times \mathbb{R} . f f is continuous if the shape of G G is contractible:
p : isContr ( esh ( G ) ) p:isContr(\esh(G))
See also
Revision on April 14, 2022 at 05:49:49 by
Anonymous? .
See the history of this page for a list of all contributions to it.