OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/PhysicalCoordinateFrame.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A physical frame gives a continuous inverse on its coordinate image

  1. def OAI.DefocusingNLS.HasPhysicalCoordinateFrame line 13
  2. theorem OAI.DefocusingNLS.physicalCoordinateFrame_of_bijective line 17
  3. def OAI.DefocusingNLS.HasPhysicalDiagonalFrame line 37
  4. theorem OAI.DefocusingNLS.physicalDiagonalFrame_of_frame line 44