New file

In this file...

Main declarations

• ConNF.foo: Something new.

@[defaultInstance 200]

instance ConNF.instDerivativeAllPerm_1 [ConNF.Params] {β γ : ConNF.TypeIndex} : ConNF.Derivative (ConNF.AllPerm β) (ConNF.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' [ConNF.Params] {β : ConNF.TypeIndex} (ρ : ConNF.AllPerm β) : ρ ⇘ ConNF.Path.nil = ρ

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

• ConNF.newSetEquiv = ConNF.castTSet ⋯ ⋯

@[simp]

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

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

Equations

• ConNF.allPermEquiv = ConNF.castAllPerm ⋯ ⋯

@[simp]

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

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

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

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

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

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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