EquivariantMixing.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Mixing

abbrev OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.MixEntries line 17
Source documentation
Index the literal children of a small family, with no uniform bound on the ranks of the family's members.
```
abbrev MixEntries (f : ι → S.Name) := Σ i, Edges (f i).raw
```
Mentions: OAI.PartitionConsistency.SetForcingNames.Edges
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mixTest line 19

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mixTest_permute line 25

Source documentation

Fixing the names and their activation conditions permutes every entry of their union mixture, including all strengthenings of all activations.

theorem mixTest_permute (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ)
    (hf : ∀ g ∈ H, ∀ i, g • f i = f i)
    (ha : ∀ g ∈ H, ∀ i, S.move g (a i) = a i) :
    ∀ g ∈ H, ∀ (i : S.MixEntries f) p, S.mixTest f a i p →
      ∃ j : S.MixEntries f, (f j.1).child j.2.property = g • (f i.1).child i.2.property ∧
        S.mixTest f a j (S.move g p) := by
…

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mix line 45
Source documentation
A coherent or antichain mixture. Coherence is a property proved separately; the present construction itself is just the unrestricted union of active names.
```
def mix (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hf : ∀ g ∈ H, ∀ i, g • f i = f i)
    (ha : ∀ g ∈ H, ∀ i, S.move g (a i) = a i) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mix_fixed line 51
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_mix line 57

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_mix line 73

Source documentation

The exact regular forcing value of membership in the union mixture.

theorem mem_mix (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hf : ∀ g ∈ H, ∀ i, g • f i = f i)
    (ha : ∀ g ∈ H, ∀ i, S.move g (a i) = a i) (ν : S.Name) (p : P) :
    S.atomic.MemF p ν (S.mix f a H hH hf ha) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i : ι, r ≤ a i ∧ S.atomic.MemF r ν (f i) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_mix_at line 100

Source documentation

Any coherent family is equal to its mixture below its activation condition. This applies in particular to antichains, when coherence is vacuous.

theorem eq_mix_at (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hf : ∀ g ∈ H, ∀ i, g • f i = f i)
    (ha : ∀ g ∈ H, ∀ i, S.move g (a i) = a i)
    (hcoh : ∀ i j p, p ≤ a i → p ≤ a j → S.atomic.EqF p (f i) (f j)) (i : ι) :
    S.atomic.EqF (a i) (S.mix f a H hH hf ha) (f i) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.equivariantMixTest_permute line 135

Source documentation

An equivariant family need not have each member fixed pointwise. Permuting the names together with their activation conditions suffices.

theorem equivariantMixTest_permute (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ)
    (hperm : ∀ g ∈ H, ∀ i, ∃ j, f j = g • f i ∧ a j = S.move g (a i)) :
    ∀ g ∈ H, ∀ (i : S.MixEntries f) p, S.mixTest f a i p →
      ∃ j : S.MixEntries f, (f j.1).child j.2.property = g • (f i.1).child i.2.property ∧
        S.mixTest f a j (S.move g p) := by
…

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.equivariantMix line 155
Source documentation
Union of an equivariant family of active arbitrary-rank names. No choice of a common strengthening occurs in the definition.
```
def equivariantMix (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hperm : ∀ g ∈ H, ∀ i, ∃ j, f j = g • f i ∧ a j = S.move g (a i)) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.equivariantMix_fixed line 160
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.edge_equivariantMix line 165

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_equivariantMix line 180

Source documentation

The exact regular forcing value of membership in the union mixture.

theorem mem_equivariantMix (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hperm : ∀ g ∈ H, ∀ i, ∃ j, f j = g • f i ∧ a j = S.move g (a i)) (ν : S.Name) (p : P) :
    S.atomic.MemF p ν (S.equivariantMix f a H hH hperm) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i : ι, r ≤ a i ∧ S.atomic.MemF r ν (f i) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.eq_equivariantMix_at line 206

Source documentation

Any coherent family is equal to its mixture below its activation condition. This applies in particular to antichains, when coherence is vacuous.

theorem eq_equivariantMix_at (f : ι → S.Name) (a : ι → P) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hperm : ∀ g ∈ H, ∀ i, ∃ j, f j = g • f i ∧ a j = S.move g (a i))
    (hcoh : ∀ i j p, p ≤ a i → p ≤ a j → S.atomic.EqF p (f i) (f j)) (i : ι) :
    S.atomic.EqF (a i) (S.equivariantMix f a H hH hperm) (f i) := by
…