OAI/Dynamics/EntropyCounterexample/MonotoneItineraries.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.MonotoneItineraries.labelSum line 10
2. lemma OAI.Problem340.MonotoneItineraries.labelSum_le line 13
3. lemma OAI.Problem340.MonotoneItineraries.eq_of_le_of_labelSum_eq line 22
4. theorem OAI.Problem340.MonotoneItineraries.card_range_le line 28
5. def OAI.Problem340.MonotoneItineraries.itinerary line 47
6. lemma OAI.Problem340.MonotoneItineraries.itinerary_monotone line 50
7. theorem OAI.Problem340.MonotoneItineraries.card_itinerary_range_le line 56