OAI/Combinatorics/SecondNeighborhood/KernelRestriction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SeymourSecondNeighborhood.Pruning.PairFiber line 12
2. def OAI.SeymourSecondNeighborhood.Pruning.fiberIndex line 14
3. theorem OAI.SeymourSecondNeighborhood.Pruning.fiberIndex_injective line 18
4. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_range_fiberIndex line 25
5. def OAI.SeymourSecondNeighborhood.Pruning.restrictFiber line 36
6. def OAI.SeymourSecondNeighborhood.Pruning.matrixD line 40
7. def OAI.SeymourSecondNeighborhood.Pruning.localSupport line 44
8. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixB_mulVec_fiber line 48
9. theorem OAI.SeymourSecondNeighborhood.Pruning.matrixN_transpose_mulVec_fiber line 65
10. theorem OAI.SeymourSecondNeighborhood.Pruning.restrictFiber_mem_kernelD line 82
11. theorem OAI.SeymourSecondNeighborhood.Pruning.restrictFiber_mem_kernelD_transpose line 101