OAI/Combinatorics/HadwigerCounterexample/UnaryRecords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Unary Records

  1. abbrev OAI.HadwigerCounterexample.Ledger line 15

    Source documentation

    records of x indexed by opposite pin plan signs

    abbrev Ledger {p : Shape} {n} (f : Plan p n) :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Plan

  2. instance OAI.HadwigerCounterexample.fintypeLedger line 18
  3. theorem OAI.HadwigerCounterexample.ledger_dim line 23
  4. def OAI.HadwigerCounterexample.entries line 29
  5. theorem OAI.HadwigerCounterexample.entries_val line 32
  6. theorem OAI.HadwigerCounterexample.entries_rows line 38
  7. theorem OAI.HadwigerCounterexample.rowAgree_step line 51
  8. def OAI.HadwigerCounterexample.Volley.promised line 61

    Source documentation

    Deterministic realization promise at two orientations. Can be required only if both accept the specific parameter pair and their keys agree.

    def promised (t : Tagging p I) (m : Mixer p n)
    (a b : Plan p n) (x y : UnitType p n N) :=
…

    Mentions: OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.UnitType

  9. theorem OAI.HadwigerCounterexample.Volley.carried_heavy line 68
  10. theorem OAI.HadwigerCounterexample.Volley.record_hit line 73