OAI/GroupTheory/PolycyclicRecognition/Algebra/ProductLocalCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extracting local coordinates from a product map

A local coordinate map of the form (x,z) ↦ (f x,z) supplies local coordinates for f. This bridge works even when the target factor has no manifold structure yet.

  1. theorem OAI.PolycyclicRecognition.local_coordinates_of_prodMap line 20
  2. theorem OAI.PolycyclicRecognition.localHomeomorph_hom_of_prodMap line 37