OAI/Analysis/CircleDomains/Selection/LevelFlowCoordinate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonstationary trajectory has nonzero speed in the actual local one-dimensional coordinate of its regular level.

  1. lemma OAI.CircleDomainRigidity.level_flow_coordinate_deriv_ne_zero line 14
  2. lemma OAI.CircleDomainRigidity.level_flow_coordinate_open_image line 43