New file

In this file...

Main declarations

• ConNF.foo: Something new.

@[defaultInstance 200]

instance ConNF.instDerivativeAllPerm_1 [Params] {β γ : TypeIndex} : Derivative (AllPerm β) (AllPerm γ) β γ

A redefinition of the derivative of allowable permutations that is invariant of level, but still has nice definitional properties.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConNF.allPerm_deriv_nil' [Params] {β : TypeIndex} (ρ : AllPerm β) : ρ ⇘ Path.nil = ρ

@[simp]

theorem ConNF.allPerm_deriv_sderiv' [Params] {β γ δ : TypeIndex} (ρ : AllPerm β) (A : β ↝ γ) (h : δ < γ) : ρ ⇘ (A ↘ h) = ρ ⇘ A ↘ h

@[simp]

theorem ConNF.allPermSderiv_forget' [Params] {β γ : TypeIndex} (h : γ < β) (ρ : AllPerm β) : (ρ ↘ h)ᵁ = ρᵁ ↘ h

@[simp]

theorem ConNF.allPerm_inv_sderiv' [Params] {β γ : TypeIndex} (h : γ < β) (ρ : AllPerm β) : ρ⁻¹ ↘ h = (ρ ↘ h)⁻¹

def ConNF.Symmetric [Params] {α β : Λ} (s : Set (TSet ↑β)) (hβ : ↑β < ↑α) : Prop

Equations

• ConNF.Symmetric s hβ = ∃ (S : ConNF.Support ↑α), ∀ (ρ : ConNF.AllPerm ↑α), ρᵁ • S = S → ρ ↘ hβ • s = s

def ConNF.newSetEquiv [Params] {α : Λ} : TSet ↑α ≃ TSet ↑α

Equations

• ConNF.newSetEquiv = ConNF.castTSet ⋯ ⋯

@[simp]

theorem ConNF.newSetEquiv_forget [Params] {α : Λ} (x : TSet ↑α) : (newSetEquiv x)ᵁ = xᵁ

def ConNF.allPermEquiv [Params] {α : Λ} : NewPerm ≃ AllPerm ↑α

Equations

• ConNF.allPermEquiv = ConNF.castAllPerm ⋯ ⋯

@[simp]

theorem ConNF.allPermEquiv_forget [Params] {α : Λ} (ρ : NewPerm) : (allPermEquiv ρ)ᵁ = ρᵁ

theorem ConNF.allPermEquiv_sderiv [Params] {α β : Λ} (ρ : NewPerm) (hβ : ↑β < ↑α) : allPermEquiv ρ ↘ hβ = ρ.sderiv ↑β

theorem ConNF.TSet.exists_of_symmetric [Params] {α β : Λ} (s : Set (TSet ↑β)) (hβ : ↑β < ↑α) (hs : Symmetric s hβ) : ∃ (x : TSet ↑α), ∀ (y : TSet ↑β), y ∈[hβ] x ↔ y ∈ s

theorem ConNF.TSet.exists_support [Params] {α : Λ} (x : TSet ↑α) : ∃ (S : Support ↑α), ∀ (ρ : AllPerm ↑α), ρᵁ • S = S → ρ • x = x

theorem ConNF.TSet.symmetric [Params] {α β : Λ} (x : TSet ↑α) (hβ : ↑β < ↑α) : Symmetric {y : TSet ↑β | y ∈[hβ] x} hβ

theorem ConNF.tSet_ext' [Params] {α β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑α) (h : ∀ (z : TSet ↑β), z ∈[hβ] x ↔ z ∈[hβ] y) : x = y

@[simp]

theorem ConNF.TSet.mem_smul_iff' [Params] {α β : TypeIndex} {x : TSet β} {y : TSet α} (h : β < α) (ρ : AllPerm α) : x ∈[h] ρ • y ↔ ρ⁻¹ ↘ h • x ∈[h] y

def ConNF.singleton [Params] {α β : Λ} (hβ : ↑β < ↑α) (x : TSet ↑β) : TSet ↑α

Equations

• ConNF.singleton hβ x = ConNF.PreCoherentData.singleton hβ x

@[simp]

theorem ConNF.typedMem_singleton_iff' [Params] {α β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑β) : y ∈[hβ] ConNF.singleton hβ x ↔ y = x

@[simp]

theorem ConNF.smul_singleton [Params] {α β : Λ} (hβ : ↑β < ↑α) (x : TSet ↑β) (ρ : AllPerm ↑α) : ρ • ConNF.singleton hβ x = ConNF.singleton hβ (ρ ↘ hβ • x)

theorem ConNF.singleton_injective [Params] {α β : Λ} (hβ : ↑β < ↑α) : Function.Injective (ConNF.singleton hβ)

@[simp]

theorem ConNF.singleton_inj [Params] {α β : Λ} {hβ : ↑β < ↑α} {x y : TSet ↑β} : ConNF.singleton hβ x = ConNF.singleton hβ y ↔ x = y

theorem ConNF.sUnion_singleton_symmetric_aux' [Params] {α β γ : Λ} (hγ : ↑γ < ↑β) (hβ : ↑β < ↑α) (s : Set (TSet ↑γ)) (S : Support ↑α) (hS : ∀ (ρ : AllPerm ↑α), ρᵁ • S = S → ρ ↘ hβ • ConNF.singleton hγ '' s = ConNF.singleton hγ '' s) (ρ : AllPerm ↑β) : ρᵁ • S.strong ↘ hβ = S.strong ↘ hβ → ρ ↘ hγ • s ⊆ s

theorem ConNF.sUnion_singleton_symmetric_aux [Params] {α β γ : Λ} (hγ : ↑γ < ↑β) (hβ : ↑β < ↑α) (s : Set (TSet ↑γ)) (S : Support ↑α) (hS : ∀ (ρ : AllPerm ↑α), ρᵁ • S = S → ρ ↘ hβ • ConNF.singleton hγ '' s = ConNF.singleton hγ '' s) (ρ : AllPerm ↑β) : ρᵁ • S.strong ↘ hβ = S.strong ↘ hβ → ρ ↘ hγ • s = s

theorem ConNF.sUnion_singleton_symmetric [Params] {α β γ : Λ} (hγ : ↑γ < ↑β) (hβ : ↑β < ↑α) (s : Set (TSet ↑γ)) (hs : Symmetric (ConNF.singleton hγ '' s) hβ) : Symmetric s hγ