New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

Equations

• x ⊔[hβ] y = (x ᶜ[hβ] ⊓[hβ] y ᶜ[hβ]) ᶜ[hβ]

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

@[simp]

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

def ConNF.higherIndex [ConNF.Params] (α : ConNF.Λ) : ConNF.Λ

Equations

• ConNF.higherIndex α = ⋯.choose

theorem ConNF.lt_higherIndex [ConNF.Params] {α : ConNF.Λ} : ↑α < ↑(ConNF.higherIndex α)

theorem ConNF.tSet_nonempty [ConNF.Params] {α : ConNF.Λ} (h : ∃ (β : ConNF.Λ), ↑β < ↑α) : Nonempty (ConNF.TSet ↑α)

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

Equations

• ConNF.empty hβ = ⋯.some ⊓[hβ] ⋯.some ᶜ[hβ]

@[simp]

theorem ConNF.mem_empty_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x : ConNF.TSet ↑β) : ¬x ∈[hβ] ConNF.empty hβ

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

Equations

• ConNF.univ hβ = (ConNF.empty hβ) ᶜ[hβ]

@[simp]

theorem ConNF.mem_univ_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x : ConNF.TSet ↑β) : x ∈[hβ] ConNF.univ hβ

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

The set of all ordered pairs.

Equations

• ConNF.orderedPairs hβ hγ hδ = ConNF.vCross hβ hγ hδ (ConNF.univ hδ)

@[simp]

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

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

Equations

• ConNF.converse hβ hγ hδ x = ConNF.converse' hβ hγ hδ x ⊓[hβ] ConNF.orderedPairs hβ hγ hδ

@[simp]

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

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

Equations

• ConNF.cross hβ hγ hδ x y = ConNF.converse hβ hγ hδ (ConNF.vCross hβ hγ hδ x) ⊓[hβ] ConNF.vCross hβ hγ hδ y

@[simp]

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

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

Equations

• ConNF.singletonImage hβ hγ hδ hε x = ConNF.singletonImage' hβ hγ hδ hε x ⊓[hβ] ConNF.cross hβ hγ hδ (ConNF.cardinalOne hδ hε) (ConNF.cardinalOne hδ hε)

@[simp]

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

theorem ConNF.exists_of_mem_singletonImage [ConNF.Params] {α β γ δ ε : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : ConNF.TSet ↑β} {z w : ConNF.TSet ↑δ} (h : ⟨z, w⟩[hγ, hδ] ∈[hβ] ConNF.singletonImage hβ hγ hδ hε x) : ∃ (a : ConNF.TSet ↑ε) (b : ConNF.TSet ↑ε), z = {a}[hε] ∧ w = {b}[hε]

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

Turn a model element encoding a relation into an actual relation.

Equations

• ConNF.ExternalRel hβ hγ hδ r x y = (⟨x, y⟩[hγ, hδ] ∈[hβ] r)

@[simp]

theorem ConNF.externalRel_converse [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.TSet ↑α) : ConNF.ExternalRel hβ hγ hδ (ConNF.converse hβ hγ hδ r) = (ConNF.ExternalRel hβ hγ hδ r).inv

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

The codomain of a relation.

Equations

• ConNF.codom hβ hγ hδ r = (ConNF.typeLower ⋯ hβ hγ hδ (ConNF.singletonImage ⋯ hβ hγ hδ r) ᶜ[⋯]) ᶜ[hδ]

@[simp]

theorem ConNF.mem_codom_iff [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.TSet ↑α) (x : ConNF.TSet ↑δ) : x ∈[hδ] ConNF.codom hβ hγ hδ r ↔ x ∈ (ConNF.ExternalRel hβ hγ hδ r).codom

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

The domain of a relation.

Equations

• ConNF.dom hβ hγ hδ r = ConNF.codom hβ hγ hδ (ConNF.converse hβ hγ hδ r)

@[simp]

theorem ConNF.mem_dom_iff [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.TSet ↑α) (x : ConNF.TSet ↑δ) : x ∈[hδ] ConNF.dom hβ hγ hδ r ↔ x ∈ (ConNF.ExternalRel hβ hγ hδ r).dom

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

The field of a relation.

Equations

• ConNF.field hβ hγ hδ r = ConNF.dom hβ hγ hδ r ⊔[hδ] ConNF.codom hβ hγ hδ r

@[simp]

theorem ConNF.mem_field_iff [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.TSet ↑α) (x : ConNF.TSet ↑δ) : x ∈[hδ] ConNF.field hβ hγ hδ r ↔ x ∈ (ConNF.ExternalRel hβ hγ hδ r).field

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

Equations

• ConNF.subset hβ hγ hδ hε = ConNF.subset' hβ hγ hδ hε ⊓[hβ] ConNF.orderedPairs hβ hγ hδ

@[simp]

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

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

Equations

• ConNF.membership hβ hγ hδ hε = ConNF.subset hβ hγ hδ hε ⊓[hβ] ConNF.cross hβ hγ hδ (ConNF.cardinalOne hδ hε) (ConNF.univ hδ)

@[simp]

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

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

Equations

• ConNF.powerset hβ hγ x = ConNF.dom ⋯ ⋯ hβ (ConNF.subset ⋯ ⋯ hβ hγ ⊓[⋯] ConNF.vCross ⋯ ⋯ hβ {x}[hβ])

@[simp]

theorem ConNF.mem_powerset_iff [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : ConNF.TSet ↑β) : x ∈[hβ] ConNF.powerset hβ hγ y ↔ x ⊆[ConNF.TSet ↑γ, hγ] y

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

The set ι²''x = {{{a}} | a ∈ x}.

Equations

• ConNF.doubleSingleton hβ hγ hδ x = ConNF.cross hβ hγ hδ x x ⊓[hβ] ConNF.cardinalOne hβ hγ

@[simp]

theorem ConNF.mem_doubleSingleton_iff [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : ConNF.TSet ↑γ) (y : ConNF.TSet ↑β) : y ∈[hβ] ConNF.doubleSingleton hβ hγ hδ x ↔ ∃ (z : ConNF.TSet ↑δ), z ∈[hδ] x ∧ y = {{z}[hδ]}[hγ]

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

The union of a set of singletons: ι⁻¹''x = {a | {a} ∈ x}.

Equations

• ConNF.singletonUnion hβ hγ x = ConNF.typeLower ⋯ ⋯ hβ hγ (ConNF.vCross ⋯ ⋯ hβ x)

@[simp]

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

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

The union of a set of sets.

singletonUnion dom {⟨{a}, b⟩ | a ∈ b} ∩ (1 × x) =
singletonUnion dom {⟨{a}, b⟩ | a ∈ b ∧ b ∈ x} =
singletonUnion {{a} | a ∈ b ∧ b ∈ x} =
{a | a ∈ b ∧ b ∈ x} =
⋃ x

Equations

• ConNF.sUnion hβ hγ x = ConNF.singletonUnion hβ hγ (ConNF.dom ⋯ ⋯ hβ (ConNF.membership ⋯ ⋯ hβ hγ ⊓[⋯] ConNF.cross ⋯ ⋯ hβ (ConNF.cardinalOne hβ hγ) x))

@[simp]

theorem ConNF.mem_sUnion_iff [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x : ConNF.TSet ↑α) (y : ConNF.TSet ↑γ) : y ∈[hγ] ConNF.sUnion hβ hγ x ↔ ∃ (t : ConNF.TSet ↑β), t ∈[hβ] x ∧ y ∈[hγ] t

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

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

Our model is κ-complete; small unions exist. In particular, the model knows the correct natural numbers.

Equations

• ConNF.smallUnion hβ s hs = ⋯.choose

@[simp]

theorem ConNF.mem_smallUnion_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (s : Set (ConNF.TSet ↑α)) (hs : ConNF.Small s) (x : ConNF.TSet ↑β) : x ∈[hβ] ConNF.smallUnion hβ s hs ↔ ∃ t ∈ s, x ∈[hβ] t