BlockOrbits.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.exists_block_perm_map line 13

Source documentation

A permutation supported on a finite block can map any two equally sized subsets of the block to one another.

theorem exists_block_perm_map {α : Type u} [Fintype α] [DecidableEq α]
    (B s t : Finset α) (hs : s ⊆ B) (ht : t ⊆ B)
    (hc : s.card = t.card) :
    ∃ π : Equiv.Perm α, (∀ u, u ∉ B → π u = u) ∧
      s.map π.toEmbedding = t := by
…

def OAI.Problem313.blockEdgeOrbit line 45
Source documentation
The edge orbit under permutations fixing the complement of B pointwise.
```
def blockEdgeOrbit {n : ℕ} (B : Finset (Fin n)) (e : GraphEdge n) :
    Finset (GraphEdge n) := by
…
```
Mentions: OAI.Problem313.GraphEdge
theorem OAI.Problem313.mem_blockEdgeOrbit line 51
theorem OAI.Problem313.block_internal_mem_orbit line 58
Source documentation
All edges wholly contained in a block are in one supported-permutation orbit.
```
theorem block_internal_mem_orbit {n : ℕ} {B : Finset (Fin n)}
    {e e' : GraphEdge n} (he : e.val ⊆ B) (he' : e'.val ⊆ B) :
    e' ∈ blockEdgeOrbit B e := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockEdgeOrbit
theorem OAI.Problem313.card_block_internal_edges line 65
Source documentation
The number of graph edges wholly contained in a vertex block.
```
theorem card_block_internal_edges {n : ℕ} (B : Finset (Fin n)) :
    (Finset.univ.filter (fun e : GraphEdge n => e.val ⊆ B)).card = B.card.choose 2 := by
…
```
Mentions: OAI.Problem313.GraphEdge
theorem OAI.Problem313.block_card_le_choose_two line 78
theorem OAI.Problem313.block_internal_orbit_card line 84
Source documentation
Internal edge orbits have at least as many edges as the block has vertices.
```
theorem block_internal_orbit_card {n : ℕ} {B : Finset (Fin n)}
    {e : GraphEdge n} (hB : 3 ≤ B.card) (he : e.val ⊆ B) :
    B.card ≤ (blockEdgeOrbit B e).card := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockEdgeOrbit
def OAI.Problem313.blockBoundaryEdge line 97
Source documentation
The boundary edge joining a vertex of the block to a fixed exterior vertex.
```
def blockBoundaryEdge {n : ℕ} {B : Finset (Fin n)} (w : Fin n) (hw : w ∉ B)
    (u : B) : GraphEdge n :=
…
```
Mentions: OAI.Problem313.GraphEdge
theorem OAI.Problem313.blockBoundaryEdge_injective line 103
theorem OAI.Problem313.block_boundary_mem_orbit line 113
Source documentation
Boundary edges with the same exterior endpoint are in one block orbit.
```
theorem block_boundary_mem_orbit {n : ℕ} {B : Finset (Fin n)}
    {e : GraphEdge n} {u w : Fin n} (hu : u ∈ B) (hw : w ∉ B)
    (he : e.val = {u, w}) (v : B) :
    blockBoundaryEdge w hw v ∈ blockEdgeOrbit B e := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockBoundaryEdge, OAI.Problem313.blockEdgeOrbit
theorem OAI.Problem313.block_boundary_orbit_card line 131
Source documentation
Boundary edge orbits contain at least one edge for every block vertex.
```
theorem block_boundary_orbit_card {n : ℕ} {B : Finset (Fin n)}
    {e : GraphEdge n} {u w : Fin n} (hu : u ∈ B) (hw : w ∉ B)
    (he : e.val = {u, w}) : B.card ≤ (blockEdgeOrbit B e).card := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockEdgeOrbit
theorem OAI.Problem313.blockEdgeOrbit_card_lower line 145
Source documentation
Every edge incident with a block of at least three vertices has a supported-permutation orbit of cardinality at least the block cardinality.
```
theorem blockEdgeOrbit_card_lower {n : ℕ} {B : Finset (Fin n)}
    {e : GraphEdge n} (hB : 3 ≤ B.card) (hmeet : (e.val ∩ B).Nonempty) :
    B.card ≤ (blockEdgeOrbit B e).card := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockEdgeOrbit