BlockOrbit.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.extendBlockPerm line 12
Source documentation
A permutation of a block, extended by the identity away from the block.
```
def extendBlockPerm {α : Type u} [DecidableEq α] (B : Finset α)
    (σ : Equiv.Perm B) : Equiv.Perm α :=
…
```
theorem OAI.Problem313.extendBlockPerm_apply_mem line 17
theorem OAI.Problem313.extendBlockPerm_apply_notMem line 23

theorem OAI.Problem313.exists_blockPerm_map line 29

Source documentation

Equal-sized subsets of a block can be mapped to one another while fixing its complement.

theorem exists_blockPerm_map {α : Type u} [DecidableEq α]
    (B s t : Finset α) (hs : s ⊆ B) (ht : t ⊆ B) (hc : s.card = t.card) :
    ∃ σ : Equiv.Perm B, s.map (extendBlockPerm B σ).toEmbedding = t := by
…

Mentions: OAI.Problem313.extendBlockPerm

theorem OAI.Problem313.extendBlockPerm_map_disjoint line 48

Source documentation

A block permutation fixes any finite set disjoint from the block.

theorem extendBlockPerm_map_disjoint {α : Type u} [DecidableEq α]
    (B s : Finset α) (σ : Equiv.Perm B) (hs : Disjoint s B) :
    s.map (extendBlockPerm B σ).toEmbedding = s := by
…

Mentions: OAI.Problem313.extendBlockPerm

theorem OAI.Problem313.exists_blockPerm_map_of_sdiff_eq line 65

Source documentation

Equal-sized finite sets with the same exterior part are in the same block orbit.

theorem exists_blockPerm_map_of_sdiff_eq {α : Type u} [DecidableEq α]
    (B s t : Finset α) (hc : s.card = t.card) (hout : s \ B = t \ B) :
    ∃ σ : Equiv.Perm B, s.map (extendBlockPerm B σ).toEmbedding = t := by
…

Mentions: OAI.Problem313.extendBlockPerm

theorem OAI.Problem313.exists_blockPerm_permEdge line 87
Source documentation
Edge transport preserving the vertices outside the selected block.
```
theorem exists_blockPerm_permEdge {n : ℕ} (B : Finset (Fin n))
    (e e' : GraphEdge n) (hout : e.1 \ B = e'.1 \ B) :
    ∃ σ : Equiv.Perm B, permEdge (extendBlockPerm B σ) e = e' := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.permEdge, OAI.Problem313.extendBlockPerm
theorem OAI.Problem313.permEdge_extendBlockPerm_of_disjoint line 95
Source documentation
Every edge not touching the block is fixed pointwise by the block action.
```
theorem permEdge_extendBlockPerm_of_disjoint {n : ℕ} (B : Finset (Fin n))
    (σ : Equiv.Perm B) (e : GraphEdge n) (he : Disjoint e.1 B) :
    permEdge (extendBlockPerm B σ) e = e := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.permEdge, OAI.Problem313.extendBlockPerm
theorem OAI.Problem313.extendBlockPerm_mem_iff line 101
theorem OAI.Problem313.extendBlockPerm_map_block line 111
theorem OAI.Problem313.extendBlockPerm_sdiff line 121
Source documentation
Block-supported permutations leave the exterior part of every finite set unchanged.
```
theorem extendBlockPerm_sdiff {α : Type u} [DecidableEq α]
    (B s : Finset α) (σ : Equiv.Perm B) :
    s.map (extendBlockPerm B σ).toEmbedding \ B = s \ B := by
…
```
Mentions: OAI.Problem313.extendBlockPerm
theorem OAI.Problem313.exists_blockPerm_permEdge_iff line 131
Source documentation
Two graph edges belong to the same block orbit exactly when their exterior vertices agree.
```
theorem exists_blockPerm_permEdge_iff {n : ℕ} (B : Finset (Fin n))
    (e e' : GraphEdge n) :
    (∃ σ : Equiv.Perm B, permEdge (extendBlockPerm B σ) e = e') ↔
      e.1 \ B = e'.1 \ B := by
…
```
Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.permEdge, OAI.Problem313.extendBlockPerm
theorem OAI.Problem313.extendBlockPerm_symm line 141
theorem OAI.Problem313.permuteConfig_extendBlockPerm_apply_of_disjoint line 147
Source documentation
Relabeling inside the block leaves each exterior configuration coordinate unchanged.
```
theorem permuteConfig_extendBlockPerm_apply_of_disjoint {n : ℕ}
    (B : Finset (Fin n)) (σ : Equiv.Perm B) (x : GraphConfig n)
    (e : GraphEdge n) (he : Disjoint e.1 B) :
    permuteConfig (extendBlockPerm B σ) x e = x e := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.GraphEdge, OAI.Problem313.permuteConfig, OAI.Problem313.extendBlockPerm