OAI/NumberTheory/TwoPoint/Circuits/CircuitAssignmentUpdates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Updates along the disjoint blocks of a canonical DNF path. These lemmas also justify recovering the original restriction after decoding a block.

  1. lemma OAI.TwoPointCorrelations.PartialAssignment.free_assign line 15
  2. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_comm line 21
  3. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_injective_of_free line 29
  4. lemma OAI.TwoPointCorrelations.PartialAssignment.assign_congr_on line 38
  5. lemma OAI.TwoPointCorrelations.CubeTerm.live_update_disjoint line 47
  6. lemma OAI.TwoPointCorrelations.CubeTerm.compatible_assign_disjoint line 55
  7. lemma OAI.TwoPointCorrelations.CubeTerm.satisfied_mono line 62