OAI/Geometry/RuledCovering/Nilpotent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RuledApproximation.swapReflect line 13

   Source documentation

   The flip and interchange relating the two physical maps.

   def swapReflect : Space ≃ₗᵢ[ℝ] Space where
   …

   Mentions: OAI.RuledApproximation.Space

2. lemma OAI.RuledApproximation.physicalMaps_relation line 28
3. lemma OAI.RuledApproximation.firstPhysicalMap_injective line 33
4. lemma OAI.RuledApproximation.firstPhysicalMap_ruled line 45
5. theorem OAI.RuledApproximation.nilpotent line 57

   Source documentation

   Nilpotent approximation, with finite oriented square tiles and both exact Euclidean physical realizations. Smoothness is more than the C1 producer needs.

   theorem nilpotent : NilpotentStatement := by
   …

   Mentions: OAI.RuledApproximation.NilpotentStatement