OAI/Algebra/DepthFive/ScheduleInterior.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.BalancedSchedule.firstLayer line 9
2. def OAI.Problem335.BalancedSchedule.finalLayer line 11
3. lemma OAI.Problem335.BalancedSchedule.indexedWord_first line 14
4. lemma OAI.Problem335.BalancedSchedule.indexedWord_final line 22
5. lemma OAI.Problem335.BalancedSchedule.firstLayer_mem_vLayers line 30
6. lemma OAI.Problem335.BalancedSchedule.vLayers_nonfinal line 33
7. def OAI.Problem335.BalancedSchedule.interiorVLayers line 45

   Source documentation

   The V positions eligible for isolated-position flips.

   def interiorVLayers {k : ℕ} (hk : 0 < k) (s : ℕ) : Finset (Fin (2 * k + s)) :=
   …

8. lemma OAI.Problem335.BalancedSchedule.interiorVLayers_subset line 48
9. lemma OAI.Problem335.BalancedSchedule.mem_interiorVLayers_iff line 51
10. lemma OAI.Problem335.BalancedSchedule.card_interiorVLayers line 68
11. lemma OAI.Problem335.BalancedSchedule.vLayers_sdiff_interiorVLayers line 72
12. lemma OAI.Problem335.BalancedSchedule.card_internalEnds_eq_two line 76
13. lemma OAI.Problem335.BalancedSchedule.interiorVLayers_degree_two line 101