OAI/Combinatorics/ParityLifts/RankedTrees.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ParityWL.RankedTree line 13
  2. inductive OAI.ParityWL.RankedTree.Ancestor line 19
  3. lemma OAI.ParityWL.RankedTree.Ancestor.trans line 27
  4. lemma OAI.ParityWL.RankedTree.Ancestor.cases' line 33
  5. lemma OAI.ParityWL.RankedTree.root_ancestor line 39
  6. theorem OAI.ParityWL.RankedTree.Ancestor.map line 46
  7. def OAI.ParityWL.RankedTree.nodeOrder line 55
  8. def OAI.ParityWL.RankedTree.enumeration line 62
  9. def OAI.ParityWL.RankedTree.indexed line 66
  10. lemma OAI.ParityWL.RankedTree.ancestor_indexed line 84
  11. lemma OAI.ParityWL.RankedTree.indexed_ancestor line 95
  12. structure OAI.ParityWL.RankedBagTree line 117

    Source documentation

    This records ordinary bag axioms, not lift solvability or any WL promise.

    structure RankedBagTree {W N : Type} (R : W → W → Prop) (t : ℕ) extends RankedTree N where
…

    Mentions: OAI.ParityWL.RankedTree

  13. def OAI.ParityWL.RankedBagTree.toIndexed line 132
  14. theorem OAI.ParityWL.no_choice_equal_decomposed line 159

    Source documentation

    Equality for every genuinely decomposed uncolored source.

    theorem no_choice_equal_decomposed {W N : Type} [Fintype W] [Fintype N]
    {t : ℕ} (C : ChoiceSystem t) (ht : 0 < t) (hn : ¬ C.Successful)
    (F : SimpleGraph W) (D : RankedBagTree (N := N) F.Adj t) :
…

    Mentions: OAI.ParityWL.ChoiceSystem, OAI.ParityWL.RankedBagTree