Documentation

ConNF.Levels.StrSet

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 #

source
@[irreducible]
def ConNF.StrSet [ConNF.Params] :
ConNF.TypeIndex → Type u
Equations
Instances For
    source
    theorem ConNF.StrSet.bot_eq [ConNF.Params] :
    ConNF.StrSet ⊥ = ConNF.Atom
    source
    theorem ConNF.StrSet.coe_eq [ConNF.Params] (α : ConNF.Λ) :
    ConNF.StrSet ↑α = ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StrSet β))
    source
    def ConNF.StrSet.botEquiv [ConNF.Params] :
    ConNF.StrSet ⊥ ≃ ConNF.Atom
    Equations
    Instances For
      source
      def ConNF.StrSet.coeEquiv [ConNF.Params] {α : ConNF.Λ} :
      ConNF.StrSet ↑α ≃ ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StrSet β))
      Equations
      Instances For
        source
        theorem ConNF.StrSet.coe_ext_iff' [ConNF.Params] {α : ConNF.Λ} {x y : ConNF.StrSet ↑α} :
        x = y ↔ ∀ (β : ConNF.TypeIndex) (hβ : β < ↑α) (z : ConNF.StrSet β), z ∈ ConNF.StrSet.coeEquiv x β hβ ↔ z ∈ ConNF.StrSet.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.

        source
        @[irreducible]
        def ConNF.StrSet.strPerm_smul [ConNF.Params] {α : ConNF.TypeIndex} :
        ConNF.StrPerm α → ConNF.StrSet α → ConNF.StrSet α
        Equations
        Instances For
          source
          theorem ConNF.StrSet.strPerm_smul_bot_def [ConNF.Params] (π : ConNF.StrPerm ⊥) (x : ConNF.StrSet ⊥) :
          ConNF.StrSet.strPerm_smul π x = ConNF.StrSet.botEquiv.symm (π ConNF.Path.nil • ConNF.StrSet.botEquiv x)
          source
          theorem ConNF.StrSet.strPerm_smul_coe_def [ConNF.Params] {α : ConNF.Λ} (π : ConNF.StrPerm ↑α) (x : ConNF.StrSet ↑α) :
          ConNF.StrSet.strPerm_smul π x = ConNF.StrSet.coeEquiv.symm fun (β : ConNF.TypeIndex) (hβ : β < ↑α) => ConNF.StrSet.strPerm_smul (π ↘ hβ) '' ConNF.StrSet.coeEquiv x β hβ
          source
          instance ConNF.StrSet.instSMulStrPerm [ConNF.Params] {α : ConNF.TypeIndex} :
          SMul (ConNF.StrPerm α) (ConNF.StrSet α)
          Equations
          • ConNF.StrSet.instSMulStrPerm = { smul := ConNF.StrSet.strPerm_smul }
          source
          theorem ConNF.StrSet.strPerm_smul_bot_def' [ConNF.Params] (π : ConNF.StrPerm ⊥) (x : ConNF.StrSet ⊥) :
          π • x = ConNF.StrSet.botEquiv.symm (π ConNF.Path.nil • ConNF.StrSet.botEquiv x)
          source
          theorem ConNF.StrSet.strPerm_smul_coe_def' [ConNF.Params] {α : ConNF.Λ} (π : ConNF.StrPerm ↑α) (x : ConNF.StrSet ↑α) :
          π • x = ConNF.StrSet.coeEquiv.symm fun (β : ConNF.TypeIndex) (hβ : β < ↑α) => ConNF.StrSet.strPerm_smul (π ↘ hβ) '' ConNF.StrSet.coeEquiv x β hβ
          source
          @[simp]
          theorem ConNF.StrSet.strPerm_smul_bot [ConNF.Params] (π : ConNF.StrPerm ⊥) (x : ConNF.StrSet ⊥) :
          ConNF.StrSet.botEquiv (π • x) = π ConNF.Path.nil • ConNF.StrSet.botEquiv x
          source
          @[simp]
          theorem ConNF.StrSet.strPerm_smul_coe [ConNF.Params] {α : ConNF.Λ} (π : ConNF.StrPerm ↑α) (x : ConNF.StrSet ↑α) :
          ConNF.StrSet.coeEquiv (π • x) = fun (β : ConNF.TypeIndex) (hβ : β < ↑α) => π ↘ hβ • ConNF.StrSet.coeEquiv x β hβ
          source
          theorem ConNF.StrSet.one_strPerm_smul [ConNF.Params] {α : ConNF.TypeIndex} (x : ConNF.StrSet α) :
          ConNF.StrSet.strPerm_smul 1 x = x
          source
          theorem ConNF.StrSet.mul_strPerm_smul [ConNF.Params] {α : ConNF.TypeIndex} (π₁ π₂ : ConNF.StrPerm α) (x : ConNF.StrSet α) :
          ConNF.StrSet.strPerm_smul (π₁ * π₂) x = ConNF.StrSet.strPerm_smul π₁ (ConNF.StrSet.strPerm_smul π₂ x)
          source
          instance ConNF.StrSet.instMulActionStrPerm [ConNF.Params] {α : ConNF.TypeIndex} :
          MulAction (ConNF.StrPerm α) (ConNF.StrSet α)
          Equations
          source
          theorem ConNF.StrSet.smul_none [ConNF.Params] {α : ConNF.Λ} (π : ConNF.StrPerm ↑α) :
          (π • ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑α) => ∅) = ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑α) => ∅

          Notation for typed membership #

          source
          class ConNF.TypedMem [ConNF.Params] (X : Type u_1) (Y : Type u_2) (β α : outParam ConNF.TypeIndex) :
          Type (max u_1 u_2)
          • typedMem : β < α → X → Y → Prop
          Instances
            source
            def ConNF.«term_∈[_]_» :
            Lean.TrailingParserDescr
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance ConNF.instTypedMemStrSet [ConNF.Params] {β α : ConNF.TypeIndex} :
              ConNF.TypedMem (ConNF.StrSet β) (ConNF.StrSet α) β α
              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem ConNF.StrSet.mem_iff [ConNF.Params] {α : ConNF.Λ} {β : ConNF.TypeIndex} {x : ConNF.StrSet β} {y : ConNF.StrSet ↑α} (h : β < ↑α) :
              x ∈[h] y ↔ x ∈ ConNF.StrSet.coeEquiv y β h
              source
              theorem ConNF.StrSet.coe_ext_iff [ConNF.Params] {α : ConNF.Λ} {x y : ConNF.StrSet ↑α} :
              x = y ↔ ∀ (β : ConNF.TypeIndex) (hβ : β < ↑α) (z : ConNF.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.

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