OAI/Combinatorics/ParityLifts/WeightedDual.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.linearFunctional_expansion line 13
  2. def OAI.ParityWL.dartNeighborsEquiv line 30
  3. def OAI.ParityWL.dartReverseEquiv line 36
  4. def OAI.ParityWL.dualVertex line 39
  5. def OAI.ParityWL.dualDart line 42
  6. def OAI.ParityWL.dualEdge line 45
  7. lemma OAI.ParityWL.dualEdge_symm line 50
  8. lemma OAI.ParityWL.dualEdge_support line 58
  9. lemma OAI.ParityWL.dual_constraint_expansion line 63
  10. lemma OAI.ParityWL.sum_subtype_indicator line 93
  11. def OAI.ParityWL.variableUnit line 98
  12. lemma OAI.ParityWL.variableUnit_sum line 103
  13. lemma OAI.ParityWL.dual_coordinate line 113
  14. lemma OAI.ParityWL.dual_rhs line 147
  15. structure OAI.ParityWL.WeightedWitness line 153

    Source documentation

    The supported, symmetric dual certificate of the actual parity-lift system.

    structure WeightedWitness (a : F →g T) (b : A → Bit) where
…

    Mentions: OAI.ParityWL.Bit

  16. theorem OAI.ParityWL.inconsistent_weightedWitness line 163