OAI/Algebra/Finitistic/Localization/SourceCornerEvaluation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.SourceImageEvaluation.map_projection_square line 8
2. def OAI.LittleFinitistic.SourceImageEvaluation.corner line 22
3. def OAI.LittleFinitistic.SourceImageEvaluation.imageCorner line 31
4. lemma OAI.LittleFinitistic.SourceImageEvaluation.corner_projection_square line 35
5. theorem OAI.LittleFinitistic.SourceImageEvaluation.completed_corner_square line 55
6. theorem OAI.LittleFinitistic.SourceImageEvaluation.imageCorner_restriction line 66

   Source documentation

   The central corner is exactly restriction of a, on actual vectors in eY.

   theorem imageCorner_restriction (e a : R) (he : e*e=e) (hc : e*a=a*e)
       (x : imageSpace (k := k) (Y := Y) e) :
   …

   Mentions: OAI.LittleFinitistic.SourceImageEvaluation.imageSpace

7. lemma OAI.LittleFinitistic.SourceImageEvaluation.selecting_action_eq_corner line 75