SelectedBarPowers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.SelectedBarPowers.comparison line 13
Source documentation
All powers on the exact selected first-block derived family are the original bar-derived powers; every resolution, scalar, action and stalk bridge is discharged.
```
def comparison (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :
    (native.obj^[r]) (SelectedFirstBlockFamily.derived Y) ≅ SelectedBaseIterates.object Y r :=
…
```
Mentions: OAI.LittleFinitistic.SelectedFirstBlockFamily.derived, OAI.LittleFinitistic.SelectedBaseIterates.object
theorem OAI.LittleFinitistic.SelectedBarPowers.isZero_iff line 22