New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

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

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

Equations

• x ⊓[hβ] y = ⋯.choose

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_⊓'_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓' ") (Lean.ParserDescr.cat `term 69))

@[simp]

theorem ConNF.mem_inter_iff [Params] {α β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑α) (z : TSet ↑β) : z ∈[hβ] x ⊓[hβ] y ↔ z ∈[hβ] x ∧ z ∈[hβ] y

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

Equations

• x ᶜ[hβ] = ⋯.choose

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_ᶜ'» 1024 1024 (Lean.ParserDescr.symbol " ᶜ'")

@[simp]

theorem ConNF.mem_compl_iff [Params] {α β : Λ} (hβ : ↑β < ↑α) (x : TSet ↑α) (z : TSet ↑β) : z ∈[hβ] x ᶜ[hβ] ↔ ¬z ∈[hβ] x

def ConNF.«term{_}[_]» : Lean.ParserDescr

Equations

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

def ConNF.«term{_}'» : Lean.ParserDescr

Equations

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

@[simp]

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

def ConNF.«term{_,_}[_]» : Lean.ParserDescr

Equations

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

def ConNF.«term{_,_}'» : Lean.ParserDescr

Equations

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

@[simp]

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

def ConNF.«term⟨_,_⟩[_,_]» : Lean.ParserDescr

Equations

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

def ConNF.«term⟨_,_⟩'» : Lean.ParserDescr

Equations

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

theorem ConNF.op_def [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : TSet ↑γ) : ⟨x, y⟩[hβ, hγ] = {{x}[hγ], {x, y}[hγ]}[hβ]

def ConNF.singletonImage' [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : TSet ↑β) : TSet ↑α

Equations

• ConNF.singletonImage' hβ hγ hδ hε x = ⋯.choose

@[simp]

theorem ConNF.singletonImage'_spec [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : TSet ↑β) (z w : TSet ↑ε) : ⟨{z}[hε], {w}[hε]⟩[hγ, hδ] ∈[hβ] singletonImage' hβ hγ hδ hε x ↔ ⟨z, w⟩[hδ, hε] ∈[hγ] x

def ConNF.insertion2' [Params] {α β γ δ ε ζ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : TSet ↑γ) : TSet ↑α

Equations

• ConNF.insertion2' hβ hγ hδ hε hζ x = ⋯.choose

@[simp]

theorem ConNF.insertion2'_spec [Params] {α β γ δ ε ζ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : TSet ↑γ) (a b c : TSet ↑ζ) : ⟨{{a}[hζ]}[hε], ⟨b, c⟩[hε, hζ]⟩[hγ, hδ] ∈[hβ] insertion2' hβ hγ hδ hε hζ x ↔ ⟨a, c⟩[hε, hζ] ∈[hδ] x

def ConNF.insertion3' [Params] {α β γ δ ε ζ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : TSet ↑γ) : TSet ↑α

Equations

• ConNF.insertion3' hβ hγ hδ hε hζ x = ⋯.choose

theorem ConNF.insertion3'_spec [Params] {α β γ δ ε ζ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : TSet ↑γ) (a b c : TSet ↑ζ) : ⟨{{a}[hζ]}[hε], ⟨b, c⟩[hε, hζ]⟩[hγ, hδ] ∈[hβ] insertion3' hβ hγ hδ hε hζ x ↔ ⟨a, b⟩[hε, hζ] ∈[hδ] x

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

Equations

• ConNF.vCross hβ hγ hδ x = ⋯.choose

@[simp]

theorem ConNF.mem_vCross_iff [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑γ) (a : TSet ↑β) : a ∈[hβ] vCross hβ hγ hδ x ↔ ∃ (b : TSet ↑δ) (c : TSet ↑δ), a = ⟨b, c⟩[hγ, hδ] ∧ c ∈[hδ] x

def ConNF.typeLower [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : TSet ↑α) : TSet ↑δ

Equations

• ConNF.typeLower hβ hγ hδ hε x = ⋯.choose

@[simp]

theorem ConNF.mem_typeLower_iff [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : TSet ↑α) (a : TSet ↑ε) : a ∈[hε] typeLower hβ hγ hδ hε x ↔ ∀ (b : TSet ↑δ), ⟨b, {a}[hε]⟩[hγ, hδ] ∈[hβ] x

def ConNF.converse' [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑α) : TSet ↑α

Equations

• ConNF.converse' hβ hγ hδ x = ⋯.choose

@[simp]

theorem ConNF.converse'_spec [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑α) (a b : TSet ↑δ) : ⟨a, b⟩[hγ, hδ] ∈[hβ] converse' hβ hγ hδ x ↔ ⟨b, a⟩[hγ, hδ] ∈[hβ] x

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

Equations

• ConNF.cardinalOne hβ hγ = ⋯.choose

@[simp]

theorem ConNF.mem_cardinalOne_iff [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (a : TSet ↑β) : a ∈[hβ] cardinalOne hβ hγ ↔ ∃ (b : TSet ↑γ), a = {b}[hγ]

def ConNF.subset' [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) : TSet ↑α

Equations

• ConNF.subset' hβ hγ hδ hε = ⋯.choose

theorem ConNF.subset'_spec [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (a b : TSet ↑δ) : ⟨a, b⟩[hγ, hδ] ∈[hβ] subset' hβ hγ hδ hε ↔ a ⊆[TSet ↑ε, hε] b