New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

def ConNF.union [Params] {α β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑α) : 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 [Params] {α β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑α) (z : TSet ↑β) : z ∈[hβ] x ⊔[hβ] y ↔ z ∈[hβ] x ∨ z ∈[hβ] y

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

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

Equations

• x ∆[hβ] y = x ⊓[hβ] y ᶜ[hβ] ⊔[hβ] x ᶜ[hβ] ⊓[hβ] y

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

@[simp]

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

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

Equations

• x \[hβ] y = x ⊓[hβ] y ᶜ[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_\'_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\' ") (Lean.ParserDescr.cat `term 70))

@[simp]

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

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

Equations

• ConNF.higherIndex α = ⋯.choose

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

A short name is chosen because of its frequency of use.

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

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

def ConNF.orderedPairs [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) : 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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑β) : x ∈[hβ] orderedPairs hβ hγ hδ ↔ ∃ (a : TSet ↑δ) (b : TSet ↑δ), x = ⟨a, b⟩[hγ, hδ]

def ConNF.converse [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑α) : 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 [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.cross [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x y : TSet ↑γ) : 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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x y : TSet ↑γ) (a : TSet ↑β) : a ∈[hβ] cross hβ hγ hδ x y ↔ ∃ (b : TSet ↑δ) (c : TSet ↑δ), a = ⟨b, c⟩[hγ, hδ] ∧ b ∈[hδ] x ∧ c ∈[hδ] y

def ConNF.singletonImage [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : TSet ↑β) : 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 [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

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

def ConNF.ExternalRel [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : Rel (TSet ↑δ) (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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : ExternalRel hβ hγ hδ (converse hβ hγ hδ r) = (ExternalRel hβ hγ hδ r).inv

def ConNF.codom [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : 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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑δ) : x ∈[hδ] codom hβ hγ hδ r ↔ x ∈ (ExternalRel hβ hγ hδ r).codom

def ConNF.dom [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : 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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑δ) : x ∈[hδ] dom hβ hγ hδ r ↔ x ∈ (ExternalRel hβ hγ hδ r).dom

def ConNF.field [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : 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 [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑δ) : x ∈[hδ] field hβ hγ hδ r ↔ x ∈ (ExternalRel hβ hγ hδ r).field

def ConNF.subset [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) : 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 [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (a b : TSet ↑δ) : ⟨a, b⟩[hγ, hδ] ∈[hβ] subset hβ hγ hδ hε ↔ a ⊆[TSet ↑ε, hε] b

@[simp]

theorem ConNF.singleton_subset_iff [Params] {α β : Λ} (hβ : ↑β < ↑α) (a : TSet ↑β) (b : TSet ↑α) : {a}[hβ] ⊆[TSet ↑β, hβ] b ↔ a ∈[hβ] b

def ConNF.membership [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) : 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 [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (a : TSet ↑ε) (b : TSet ↑δ) : ⟨{a}[hε], b⟩[hγ, hδ] ∈[hβ] membership hβ hγ hδ hε ↔ a ∈[hε] b

def ConNF.powerset [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x : TSet ↑β) : 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 [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : TSet ↑β) : x ∈[hβ] powerset hβ hγ y ↔ x ⊆[TSet ↑γ, hγ] y

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

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

Equations

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

@[simp]

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

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

The union of a set of singletons: ι⁻¹''x = {a | {a} ∈ x}. Scott Fenton calls this the "unit union".

Equations

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

@[simp]

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

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

The set of singletons of a set: ι''x = {{a} | a ∈ x}. Scott Fenton calls this the "unit powerset".

Equations

• ConNF.singletons hβ hγ x = ConNF.singletonUnion ⋯ hβ (ConNF.doubleSingletons ⋯ hβ hγ x)

@[simp]

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

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

The union of a set of sets.

⋃ x =
{a | a ∈ b ∧ b ∈ x} =
singletonUnion {{a} | a ∈ b ∧ b ∈ x} =
singletonUnion dom {⟨{a}, b⟩ | a ∈ b ∧ b ∈ x} =
singletonUnion dom ({⟨{a}, b⟩ | a ∈ b} ∩ (1 × 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 [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x : TSet ↑α) (y : TSet ↑γ) : y ∈[hγ] sUnion hβ hγ x ↔ ∃ (t : TSet ↑β), t ∈[hβ] x ∧ y ∈[hγ] t

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

The set of all ordered triples.

Equations

• ConNF.orderedTriples hβ hγ hδ hε hζ = ConNF.cross hβ hγ hδ (ConNF.doubleSingletons hδ hε hζ (ConNF.univ hζ)) (ConNF.vCross hδ hε hζ (ConNF.univ hζ))

@[simp]

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

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

Equations

• ConNF.insertion2 hβ hγ hδ hε hζ x = ConNF.insertion2' hβ hγ hδ hε hζ x ⊓[hβ] ConNF.orderedTriples hβ hγ hδ hε hζ

@[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 = ConNF.insertion3' hβ hγ hδ hε hζ x ⊓[hβ] ConNF.orderedTriples hβ hγ hδ hε hζ

@[simp]

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.preimage [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑γ) : TSet ↑γ

The preimage of a set under a relation.

Equations

• ConNF.preimage hβ hγ hδ r x = ConNF.dom hβ hγ hδ (r ⊓[hβ] ConNF.vCross hβ hγ hδ x)

@[simp]

theorem ConNF.mem_preimage_iff [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑γ) (y : TSet ↑δ) : y ∈[hδ] preimage hβ hγ hδ r x ↔ y ∈ (ExternalRel hβ hγ hδ r).preimage {a : TSet ↑δ | a ∈[hδ] x}

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

The image of a set under a relation.

Equations

• ConNF.image hβ hγ hδ r x = ConNF.preimage hβ hγ hδ (ConNF.converse hβ hγ hδ r) x

@[simp]

theorem ConNF.mem_image_iff [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (x : TSet ↑γ) (y : TSet ↑δ) : y ∈[hδ] image hβ hγ hδ r x ↔ y ∈ (ExternalRel hβ hγ hδ r).image {a : TSet ↑δ | a ∈[hδ] x}

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

def ConNF.smallUnion [Params] {α β : Λ} (hβ : ↑β < ↑α) (s : Set (TSet ↑α)) (hs : Small s) : 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 [Params] {α β : Λ} (hβ : ↑β < ↑α) (s : Set (TSet ↑α)) (hs : Small s) (x : TSet ↑β) : x ∈[hβ] smallUnion hβ s hs ↔ ∃ t ∈ s, x ∈[hβ] t