OAI/Combinatorics/SecondNeighborhood/KernelBasisLifts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeymourSecondNeighborhood.Pruning.extendSelected line 12
  2. theorem OAI.SeymourSecondNeighborhood.Pruning.extendSelected_apply_of_ne line 16
  3. theorem OAI.SeymourSecondNeighborhood.Pruning.extendSelected_apply_selected line 23
  4. theorem OAI.SeymourSecondNeighborhood.Pruning.mulVec_extendSelected line 33
  5. def OAI.SeymourSecondNeighborhood.Pruning.liftCoefficients line 40
  6. theorem OAI.SeymourSecondNeighborhood.Pruning.liftCoefficients_spec line 45
  7. def OAI.SeymourSecondNeighborhood.Pruning.kernelLift line 51
  8. theorem OAI.SeymourSecondNeighborhood.Pruning.kernelLift_eq line 56
  9. theorem OAI.SeymourSecondNeighborhood.Pruning.mulVec_kernelLift line 63
  10. theorem OAI.SeymourSecondNeighborhood.Pruning.kernelLift_apply_of_ne line 70
  11. theorem OAI.SeymourSecondNeighborhood.Pruning.kernelLift_normalized line 79
  12. theorem OAI.SeymourSecondNeighborhood.Pruning.exists_normalized_kernelLifts line 93
  13. theorem OAI.SeymourSecondNeighborhood.Pruning.exists_normalized_kernelLifts_of_det_ne_zero line 107