Code

WIP Manifolds#30

Code

Draft

siraben wants to merge 14 commits intoWIP_EuclideanSpacescoq-community/topology:WIP_EuclideanSpacesfrom manifoldscoq-community/topology:manifoldsCopy head branch name to clipboard

+704

Commits

Commits on Aug 20, 2023

• Add Manifolds

  

  siraben

  authored and

  Columbus240

  committed
  5a250db

  Copy full SHA for 5a250db

• Preliminary definitions

  

  siraben

  authored and

  Columbus240

  committed
  49df081

  Copy full SHA for 49df081

• Prove locally_homeomorphic is reflexive

  

  siraben

  authored and

  Columbus240

  committed
  d683ef9

  Copy full SHA for d683ef9

• Change definition of locally_homeomorphic

  

  siraben

  authored and

  Columbus240

  committed
  8001c35

  Copy full SHA for 8001c35

• Reorder imports

  

  siraben

  authored and

  Columbus240

  committed
  811b6ca

  Copy full SHA for 811b6ca

• Add additional lemmas

  

  siraben

  authored and

  Columbus240

  committed
  fb582ee

  Copy full SHA for fb582ee

• Move lemma that id is a homeomorphism

  Columbus240

  committed
  e1402bd

  Copy full SHA for e1402bd

• Restrictions of homeomorphisms are homeomorphisms

  Show description for 93ac396
  Columbus240

  committed
  93ac396

  Copy full SHA for 93ac396

• Begin proof that RTop and ℝ¹ are homeomorphic

  Columbus240

  committed
  922560b

  Copy full SHA for 922560b

• TMP: Use the new formalisation of euclidean spaces

  Columbus240

  committed
  4c48ad3

  Copy full SHA for 4c48ad3

• Study invariance of dimension and local homeo.

  Columbus240

  committed
  dd23f78

  Copy full SHA for dd23f78

• Manifolds: more on transitivity of locally homeo.

  Columbus240

  committed
  778bbd6

  Copy full SHA for 778bbd6

• TMP: Add conjectures about classification of mfds

  Columbus240

  committed
  4f35788

  Copy full SHA for 4f35788

• TMP: Do some more on manifolds

  Columbus240

  committed
  014c7f2

  Copy full SHA for 014c7f2