Structural sets

In this file, we define structural sets, which serve as the environment inside which we will construct the types of our model

Main declarations

• ConNF.StrSet: The type family of structural sets.

@[irreducible]

def ConNF.StrSet [Params] : TypeIndex → Type u

Equations

• ConNF.StrSet none = ConNF.Atom
• ConNF.StrSet (some α) = ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StrSet β))

theorem ConNF.StrSet.bot_eq [Params] : StrSet ⊥ = Atom

theorem ConNF.StrSet.coe_eq [Params] (α : Λ) : StrSet ↑α = ((β : TypeIndex) → β < ↑α → Set (StrSet β))

def ConNF.StrSet.botEquiv [Params] : StrSet ⊥ ≃ Atom

Equations

• ConNF.StrSet.botEquiv = Equiv.cast ⋯

def ConNF.StrSet.coeEquiv [Params] {α : Λ} : StrSet ↑α ≃ ((β : TypeIndex) → β < ↑α → Set (StrSet β))

Equations

• ConNF.StrSet.coeEquiv = Equiv.cast ⋯

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

Extensionality for structural sets at proper type indices. If two structural sets have the same extensions at every lower type index, then they are the same.

@[irreducible]

def ConNF.StrSet.strPerm_smul [Params] {α : TypeIndex} : StrPerm α → StrSet α → StrSet α

Equations

• ConNF.StrSet.strPerm_smul π x_3 = ConNF.StrSet.botEquiv.symm (π ConNF.Path.nil • ConNF.StrSet.botEquiv x_3)
• ConNF.StrSet.strPerm_smul π x_3 = ConNF.StrSet.coeEquiv.symm fun (β : ConNF.TypeIndex) (hβ : β < ↑α) => ConNF.StrSet.strPerm_smul (π ↘ hβ) '' ConNF.StrSet.coeEquiv x_3 β hβ

theorem ConNF.StrSet.strPerm_smul_bot_def [Params] (π : StrPerm ⊥) (x : StrSet ⊥) : strPerm_smul π x = botEquiv.symm (π Path.nil • botEquiv x)

theorem ConNF.StrSet.strPerm_smul_coe_def [Params] {α : Λ} (π : StrPerm ↑α) (x : StrSet ↑α) : strPerm_smul π x = coeEquiv.symm fun (β : TypeIndex) (hβ : β < ↑α) => strPerm_smul (π ↘ hβ) '' coeEquiv x β hβ

instance ConNF.StrSet.instSMulStrPerm [Params] {α : TypeIndex} : SMul (StrPerm α) (StrSet α)

Equations

• ConNF.StrSet.instSMulStrPerm = { smul := ConNF.StrSet.strPerm_smul }

theorem ConNF.StrSet.strPerm_smul_bot_def' [Params] (π : StrPerm ⊥) (x : StrSet ⊥) : π • x = botEquiv.symm (π Path.nil • botEquiv x)

theorem ConNF.StrSet.strPerm_smul_coe_def' [Params] {α : Λ} (π : StrPerm ↑α) (x : StrSet ↑α) : π • x = coeEquiv.symm fun (β : TypeIndex) (hβ : β < ↑α) => strPerm_smul (π ↘ hβ) '' coeEquiv x β hβ

@[simp]

theorem ConNF.StrSet.strPerm_smul_bot [Params] (π : StrPerm ⊥) (x : StrSet ⊥) : botEquiv (π • x) = π Path.nil • botEquiv x

@[simp]

theorem ConNF.StrSet.strPerm_smul_coe [Params] {α : Λ} (π : StrPerm ↑α) (x : StrSet ↑α) : coeEquiv (π • x) = fun (β : TypeIndex) (hβ : β < ↑α) => π ↘ hβ • coeEquiv x β hβ

theorem ConNF.StrSet.one_strPerm_smul [Params] {α : TypeIndex} (x : StrSet α) : strPerm_smul 1 x = x

theorem ConNF.StrSet.mul_strPerm_smul [Params] {α : TypeIndex} (π₁ π₂ : StrPerm α) (x : StrSet α) : strPerm_smul (π₁ * π₂) x = strPerm_smul π₁ (strPerm_smul π₂ x)

instance ConNF.StrSet.instMulActionStrPerm [Params] {α : TypeIndex} : MulAction (StrPerm α) (StrSet α)

Equations

• ConNF.StrSet.instMulActionStrPerm = { toSMul := ConNF.StrSet.instSMulStrPerm, one_smul := ⋯, mul_smul := ⋯ }

theorem ConNF.StrSet.smul_none [Params] {α : Λ} (π : StrPerm ↑α) : (π • coeEquiv.symm fun (x : TypeIndex) (x_1 : x < ↑α) => ∅) = coeEquiv.symm fun (x : TypeIndex) (x_1 : x < ↑α) => ∅

Notation for typed membership

class ConNF.TypedMem [Params] (X : Type u_1) (Y : Type u_2) (β α : outParam TypeIndex) : Type (max u_1 u_2)

• typedMem : β < α → X → Y → Prop

def ConNF.«term_∈[_]_» : Lean.TrailingParserDescr

Equations

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

def ConNF.«term_∈'_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_∈'_» = Lean.ParserDescr.trailingNode `ConNF.«term_∈'_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈' ") (Lean.ParserDescr.cat `term 50))

def ConNF.typedSubset [Params] (X : Type u_1) {Y : Type u_2} {β α : TypeIndex} [TypedMem X Y β α] (h : β < α) (a b : Y) : Prop

Equations

• (a ⊆[X, h] b) = ∀ (x : X), x ∈[h] a → x ∈[h] b

def ConNF.«term_⊆[_,_]_» : Lean.TrailingParserDescr

Equations

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

def ConNF.«term_⊆[_]_» : Lean.TrailingParserDescr

Equations

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

instance ConNF.instTypedMemStrSet [Params] {β α : TypeIndex} : TypedMem (StrSet β) (StrSet α) β α

Equations

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

theorem ConNF.StrSet.mem_iff [Params] {α : Λ} {β : TypeIndex} {x : StrSet β} {y : StrSet ↑α} (h : β < ↑α) : x ∈[h] y ↔ x ∈ coeEquiv y β h

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

Extensionality for structural sets at proper type indices. If two structural sets have the same extensions at every lower type index, then they are the same.

theorem ConNF.StrSet.mem_smul_iff [Params] {α β : TypeIndex} {x : StrSet β} {y : StrSet α} (h : β < α) (π : StrPerm α) : x ∈[h] π • y ↔ (π ↘ h)⁻¹ • x ∈[h] y