OAI/Combinatorics/SharpThreshold/BlockRestrictionSymmetry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem313.EdgeTouches line 9

    Source documentation

    An edge is free in a block restriction when it touches the block.

    def EdgeTouches {n : ℕ} (B : Finset (Fin n)) (e : GraphEdge n) : Prop :=
…

    Mentions: OAI.Problem313.GraphEdge

  2. def OAI.Problem313.SupportedOnBlock line 13

    Source documentation

    The vertex permutation is supported on the block.

    def SupportedOnBlock {n : ℕ} (B : Finset (Fin n))
    (π : Equiv.Perm (Fin n)) : Prop :=
…
  3. lemma OAI.Problem313.supportedOnBlock_mem_iff line 17
  4. lemma OAI.Problem313.supportedOnBlock_symm line 30
  5. lemma OAI.Problem313.block_mem_permEdge_iff line 37
  6. lemma OAI.Problem313.edgeTouches_permEdge_iff line 42
  7. lemma OAI.Problem313.permEdge_eq_self_of_not_touches line 53
  8. lemma OAI.Problem313.edgeTouches_iff_not_disjoint line 70
  9. lemma OAI.Problem313.supportedOnBlock_one line 75
  10. lemma OAI.Problem313.supportedOnBlock_mul line 80
  11. def OAI.Problem313.blockPermutationSubgroup line 88

    Source documentation

    The subgroup of permutations supported on a given vertex block.

    def blockPermutationSubgroup {n : ℕ} (B : Finset (Fin n)) :
    Subgroup (Equiv.Perm (Fin n)) where
…
  12. lemma OAI.Problem313.mem_blockPermutationSubgroup line 95
  13. lemma OAI.Problem313.supportedOnBlock_swap line 99