OAI/Algebra/Finitistic/Selected/SelectedBarStart.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SelectedBarStart.startIso line 14

   Source documentation

   Bar iteration starts at exactly the same first-block derived stalk as the ordinary simulation, through the actual extension and localization isomorphisms.

   def startIso (Y : FiniteSelectionFamily.S.{0}) :
       object Y 0 ≅ SelectedFirstBlockFamily.derived Y :=
   …

   Mentions: OAI.LittleFinitistic.SelectedFirstBlockFamily.derived

2. theorem OAI.LittleFinitistic.SelectedBarStart.start_zero line 19
3. theorem OAI.LittleFinitistic.SelectedBarStart.firstBlock_extinction line 24

   Source documentation

   The selected first-block stalk family has the exact original H-extinction.

   theorem firstBlock_extinction (m : ℕ) [NeZero m] :
       (∀ j < m, ¬ IsZero (SelectedFirstBlockFamily.derived
         ((FiniteSelectionFamily.H^[j]) (FiniteSelectionFamily.test m)))) ∧
       IsZero (SelectedFirstBlockFamily.derived
         ((FiniteSelectionFamily.H^[m]) (FiniteSelectionFamily.test m))) := by
   …

   Mentions: OAI.LittleFinitistic.SelectedFirstBlockFamily.derived, OAI.LittleFinitistic.FiniteSelectionFamily.H, OAI.LittleFinitistic.FiniteSelectionFamily.test