Code

Metric Spaces are Normal#1002

Code

Merged

affeldt-aist merged 7 commits intomath-comp:mastermath-comp/analysis:masterfrom zstone1:metric_normalzstone1/analysis:metric_normalCopy head branch name to clipboardAug 22, 2023

+236-50

Commits

Commits on Aug 9, 2023

• equivalences of normal

  zstone1

  committed
  cd196f1

• fixing tietze and pseudometrics are normal

  zstone1

  committed
  46a867b

• some linting and changelog

  zstone1

  committed
  0f669db

• small lint

  zstone1

  committed
  66c894b

• normal_spaceP w.o. R : realType paramater

  Show description for 885e98c
  affeldt-aist

  committed
  885e98c

• fix changelog

  affeldt-aist

  committed
  b731cbe

Commits on Aug 13, 2023

• simplifying dependencies

  zstone1

  committed
  ff5e932