OAI/Algebra/Finitistic/Selected/SelectedWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LittleFinitistic.SelectedWindow.Window line 10

   Source documentation

   A common finite support window chosen from the fixed representatives alone.

   structure Window where
   …

2. instance OAI.LittleFinitistic.SelectedWindow.(instance at line 17) line 17
3. def OAI.LittleFinitistic.SelectedWindow.window line 26
4. abbrev OAI.LittleFinitistic.SelectedWindow.lo line 27
5. abbrev OAI.LittleFinitistic.SelectedWindow.hi line 28
6. theorem OAI.LittleFinitistic.SelectedWindow.bounded line 31

   Source documentation

   Every term outside the fixed total's resulting support window is zero.

   theorem bounded (n : ℤ) (hn : n < lo - 2 ∨ hi < n) : IsZero (bimodule.X n) :=
   …

   Mentions: OAI.LittleFinitistic.SelectedWindow.lo, OAI.LittleFinitistic.SelectedWindow.hi

7. theorem OAI.LittleFinitistic.SelectedWindow.verified line 36

   Source documentation

   The support choices retain the complete proved rectification certificate.

   theorem verified : RectificationLemma.Verified P D0 D1 D2 f g relations lo hi :=
   …

   Mentions: OAI.LittleFinitistic.RectificationLemma.Verified, OAI.LittleFinitistic.SelectedWindow.lo, OAI.LittleFinitistic.SelectedWindow.hi