OAI/NumberTheory/Ostmann/Construction/ScheduledAnchorMatchingCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Code-preserving matchings of the actual scheduled bulk slots

  1. def OAI.Ostmann.scheduledBulkAnchorCode line 12
  2. def OAI.Ostmann.PreservesScheduledAnchorCode line 18

    Source documentation

    This is the code of the actual leaf path, independent of its labeled position inside that leaf.

    def PreservesScheduledAnchorCode {I : Type*} (role : I → CopyScheduleRole)
    (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
    (e : PartitionMatching (scheduledBulkLabel role n) (scheduledBulkLabel role n)) : Prop :=
…

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.PartitionMatching, OAI.Ostmann.scheduledBulkLabel

  3. theorem OAI.Ostmann.card_scheduled_bulk_anchor_matching line 25
  4. theorem OAI.Ostmann.scheduled_anchor_matching_count line 46
  5. def OAI.Ostmann.scheduledAnchorMatchingSet line 74
  6. theorem OAI.Ostmann.scheduledAnchorMatchingSet_card_le line 80
  7. theorem OAI.Ostmann.mem_scheduledAnchorMatchingSet line 87
  8. theorem OAI.Ostmann.scheduledAnchorMatchingSet_subset line 100