Homotopy Type Theory Sandbox

metric spaces

  • reflexive: for all xSx \in S and ϵ +\epsilon \in \mathbb{R}_+, x ϵxx \sim_\epsilon x.

  • symmetric: for all xSx \in S, ySy \in S, and ϵ +\epsilon \in \mathbb{R}_+, x ϵyx \sim_\epsilon y implies that y ϵxy \sim_\epsilon x.

  • additively transitive: for all xSx \in S, ySy \in S, zSz \in S, ϵ +\epsilon \in \mathbb{R}_+, and δ +\delta \in \mathbb{R}_+, x ϵyx \sim_\epsilon y and y δzy \sim_\delta z implies that x ϵ+δzx \sim_{\epsilon + \delta} z.

  • separation: for all xSx \in S and ySy \in S, if x ϵyx \sim_\epsilon y for all ϵ +\epsilon \in \mathbb{R}_+, then x=yx = y.

Last revised on November 18, 2024 at 18:07:35. See the history of this page for a list of all contributions to it.