def ConNF.mem [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (h : β < α) (tβ : ConNF.TSet ↑β) (tα : ConNF.TSet ↑α) : Prop

Equations

• (tβ ∈[h] tα) = (ConNF.toStructSet tβ ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet tα) ↑β ⋯)

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

Equations

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

theorem ConNF.tSet_mk_aux [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : Set (ConNF.TSet ↑β)) (hs : ∃ (S : Set (ConNF.Address ↑α)), ConNF.Small S ∧ ∀ (ρ : ConNF.Allowable ↑α), (∀ c ∈ S, ρ • c = c) → (ConNF.cons hβ) ρ • s = s) : ∃ (S : Set (ConNF.Address ↑α)), ConNF.Small S ∧ ∀ (ρ : ConNF.NewAllowable), (∀ c ∈ S, ρ • c = c) → ↑ρ ↑β • s = s

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

Equations

• ConNF.Symmetric hβ s = ∃ (S : Set (ConNF.Address ↑α)), ConNF.Small S ∧ ∀ (ρ : ConNF.Allowable ↑α), (∀ c ∈ S, ρ • c = c) → (ConNF.cons hβ) ρ • s = s

theorem ConNF.Symmetric.ofSubset [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : Set (ConNF.TSet ↑β)) : (∃ (S : Set (ConNF.Address ↑α)), ConNF.Small S ∧ ∀ (ρ : ConNF.Allowable ↑α), (∀ c ∈ S, ρ • c = c) → (ConNF.cons hβ) ρ • s ⊆ s) → ConNF.Symmetric hβ s

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

Equations

• ConNF.ModelData.TSet.mk hβ s hs = (ConNF.tSetEquiv α).symm (ConNF.NewTSet.intro s ⋯)

theorem ConNF.ModelData.TSet.toStructSet_eq [ConNF.Params] {α : ConNF.Λ} (t : ConNF.TSet ↑α) : ConNF.toStructSet t = ConNF.NewTSet.toStructSet ((ConNF.tSetEquiv α) t)

theorem ConNF.ModelData.TSet.mem_tSetEquiv_iff [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : ConNF.TSet ↑β) (t : ConNF.TSet ↑α) : s ∈[hβ] t ↔ ConNF.toStructSet s ∈ ConNF.StructSet.ofCoe (ConNF.NewTSet.toStructSet ((ConNF.tSetEquiv α) t)) ↑β ⋯

theorem ConNF.ModelData.TSet.ofCoe_toStructSet_apply_eq [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑α) : ConNF.StructSet.ofCoe (ConNF.toStructSet t) ↑β ⋯ = {p : ConNF.StructSet ↑β | ∃ s ∈ (↑((ConNF.tSetEquiv α) t)).members β, ConNF.toStructSet s = p}

@[simp]

theorem ConNF.ModelData.TSet.mem_mk_iff [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : Set (ConNF.TSet ↑β)) (hs : ConNF.Symmetric hβ s) (t : ConNF.TSet ↑β) : t ∈[hβ] ConNF.ModelData.TSet.mk hβ s hs ↔ t ∈ s

theorem ConNF.ModelData.TSet.eq_toStructSet_of_mem [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑α) (t₂ : ConNF.StructSet ↑β) : t₂ ∈ ConNF.StructSet.ofCoe (ConNF.NewTSet.toStructSet ((ConNF.tSetEquiv α) t₁)) ↑β ⋯ → ∃ (t₂' : ConNF.TSet ↑β), t₂ = ConNF.toStructSet t₂'

theorem ConNF.ModelData.TSet.ext [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (t₁ : ConNF.TSet ↑α) (t₂ : ConNF.TSet ↑α) : (∀ (s : ConNF.TSet ↑β), s ∈[hβ] t₁ ↔ s ∈[hβ] t₂) → t₁ = t₂

theorem ConNF.ModelData.TSet.smul_mem_smul [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : ConNF.TSet ↑β) (t : ConNF.TSet ↑α) (ρ : ConNF.Allowable ↑α) (h : s ∈[hβ] t) : (ConNF.cons hβ) ρ • s ∈[hβ] ρ • t

theorem ConNF.ModelData.TSet.smul_mem_smul_iff [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : ConNF.TSet ↑β) (t : ConNF.TSet ↑α) (ρ : ConNF.Allowable ↑α) : (ConNF.cons hβ) ρ • s ∈[hβ] ρ • t ↔ s ∈[hβ] t

theorem ConNF.ModelData.TSet.smul_mem_iff [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : ConNF.TSet ↑β) (t : ConNF.TSet ↑α) (ρ : ConNF.Allowable ↑α) : (ConNF.cons hβ) ρ • s ∈[hβ] t ↔ s ∈[hβ] ρ⁻¹ • t

theorem ConNF.ModelData.TSet.mem_smul_iff [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (s : ConNF.TSet ↑β) (t : ConNF.TSet ↑α) (ρ : ConNF.Allowable ↑α) : s ∈[hβ] ρ • t ↔ ((ConNF.cons hβ) ρ)⁻¹ • s ∈[hβ] t

theorem ConNF.ModelData.TSet.exists_support [ConNF.Params] {α : ConNF.Λ} (t : ConNF.TSet ↑α) : ∃ (S : Set (ConNF.Address ↑α)), ConNF.Small S ∧ MulAction.Supports (ConNF.Allowable ↑α) S t

theorem ConNF.ModelData.TSet.induction [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} (hβ : β < α) (t : ConNF.TSet ↑α) : ∃ (s : Set (ConNF.TSet ↑β)) (hs : ConNF.Symmetric hβ s), t = ConNF.ModelData.TSet.mk hβ s hs

theorem ConNF.Small.symmetric [ConNF.Params] {β : ConNF.Λ} {α : ConNF.Λ} {s : Set (ConNF.TSet ↑β)} (hs : ConNF.Small s) (hβ : β < α) : ConNF.Symmetric hβ s