OAI/Combinatorics/SecondNeighborhood/ExtremalImages.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeymourSecondNeighborhood.Extremal.diagonal line 16
  2. def OAI.SeymourSecondNeighborhood.Extremal.column line 19
  3. def OAI.SeymourSecondNeighborhood.Extremal.row line 22
  4. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_diagonal line 25
  5. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_mem line 29
  6. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_column line 32
  7. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_row line 36
  8. theorem OAI.SeymourSecondNeighborhood.Extremal.column_leftImage line 40
  9. theorem OAI.SeymourSecondNeighborhood.Extremal.row_rightImage line 46
  10. theorem OAI.SeymourSecondNeighborhood.Extremal.card_eq_sum_card_column line 52
  11. theorem OAI.SeymourSecondNeighborhood.Extremal.card_eq_sum_card_row line 59
  12. theorem OAI.SeymourSecondNeighborhood.Extremal.strict_leftImage_growth line 66
  13. theorem OAI.SeymourSecondNeighborhood.Extremal.strict_rightImage_growth line 81