Small sets

In this file, we define the notion of a small set, and prove many of the basic properties of small sets.

def ConNF.Small [ConNF.Params] {α : Type u} (s : Set α) : Prop

We say that a set is small if its cardinality is less than #κ.

Equations

• ConNF.Small s = (Cardinal.mk ↑s < Cardinal.mk ConNF.κ)

theorem ConNF.Small.lt [ConNF.Params] {α : Type u} {s : Set α} : ConNF.Small s → Cardinal.mk ↑s < Cardinal.mk ConNF.κ

Criteria for smallness

theorem ConNF.small_of_subsingleton [ConNF.Params] {α : Type u} {s : Set α} (h : s.Subsingleton) : ConNF.Small s

Subsingletons are small.

@[simp]

theorem ConNF.small_empty [ConNF.Params] {α : Type u} : ConNF.Small ∅

The empty set is small.

@[simp]

theorem ConNF.small_singleton [ConNF.Params] {α : Type u} (x : α) : ConNF.Small {x}

Singletons are small.

theorem ConNF.Small.mono [ConNF.Params] {α : Type u} {s t : Set α} (h : s ⊆ t) : ConNF.Small t → ConNF.Small s

Subsets of small sets are small. We say that the 'smallness' relation is monotone.

theorem ConNF.Small.congr [ConNF.Params] {α : Type u} {s t : Set α} (h : s = t) : ConNF.Small t → ConNF.Small s

If two sets are equal and one is small, then the other is small.

theorem ConNF.small_union [ConNF.Params] {α : Type u} {s t : Set α} (hs : ConNF.Small s) (ht : ConNF.Small t) : ConNF.Small (s ∪ t)

Binary unions of small sets are small.

theorem ConNF.small_symmDiff [ConNF.Params] {α : Type u} {s t : Set α} (hs : ConNF.Small s) (ht : ConNF.Small t) : ConNF.Small (symmDiff s t)

The symmetric difference of two small sets is small; recall that the symmetric difference s ∆ t of two sets s and t is the union of their differences: s ∆ t = s \ t ∪ t \ s.

theorem ConNF.small_iUnion [ConNF.Params] {ι α : Type u} (hι : Cardinal.mk ι < Cardinal.mk ConNF.κ) {f : ι → Set α} (hf : ∀ (i : ι), ConNF.Small (f i)) : ConNF.Small (⋃ (i : ι), f i)

An indexed union of sets is small if the index type is small and each set mentioned is small.

theorem ConNF.small_iUnion_Prop [ConNF.Params] {α : Type u} {p : Prop} {f : p → Set α} (hf : ∀ (i : p), ConNF.Small (f i)) : ConNF.Small (⋃ (i : p), f i)

It is occasionally useful to take an indexed union over the proofs of a proposition, for example when taking a union over the elements of some set. In these cases, if the resulting set is small for every proof, the union is also small.

theorem ConNF.small_biUnion [ConNF.Params] {ι α : Type u} {s : Set ι} (hs : ConNF.Small s) {f : (i : ι) → i ∈ s → Set α} (hf : ∀ (i : ι) (hi : i ∈ s), ConNF.Small (f i hi)) : ConNF.Small (⋃ (i : ι), ⋃ (hi : i ∈ s), f i hi)

A small set-indexed union of sets is small.

theorem ConNF.Small.image [ConNF.Params] {α β : Type u} {s : Set α} (f : α → β) : ConNF.Small s → ConNF.Small (f '' s)

The image of a small set under any function f is small.

theorem ConNF.Small.preimage [ConNF.Params] {α β : Type u} {s : Set α} (f : β → α) (h : Function.Injective f) : ConNF.Small s → ConNF.Small (f ⁻¹' s)

The preimage of a small set under an injective function f is small.

theorem ConNF.κ_le_of_not_small [ConNF.Params] {α : Type u} {s : Set α} (h : ¬ConNF.Small s) : Cardinal.mk ConNF.κ ≤ Cardinal.mk ↑s

If a set is not small, its cardinality is larger than #κ.

theorem ConNF.iio_small [ConNF.Params] (i : ConNF.κ) : ConNF.Small {j : ConNF.κ | j < i}

Initial segments of κ (excluding the endpoint) are small.

theorem ConNF.iic_small [ConNF.Params] (i : ConNF.κ) : ConNF.Small {j : ConNF.κ | j ≤ i}

Initial segments of κ (including the endpoint) are small.

Cardinality bounds on collections of small sets

theorem ConNF.card_le_card_small [ConNF.Params] (α : Type u) : Cardinal.mk α ≤ Cardinal.mk ↑{s : Set α | ConNF.Small s}

The amount of small subsets of any type α is bounded below by the cardinality of α.

theorem ConNF.card_small_le [ConNF.Params] {α : Type u} (h : Cardinal.mk α ≤ Cardinal.mk ConNF.μ) : Cardinal.mk ↑{s : Set α | ConNF.Small s} ≤ Cardinal.mk ConNF.μ

Because μ is a strong limit, there are at most μ small subsets of a type at most as large as μ.

theorem ConNF.card_small_eq [ConNF.Params] {α : Type u} (h : Cardinal.mk α = Cardinal.mk ConNF.μ) : Cardinal.mk ↑{s : Set α | ConNF.Small s} = Cardinal.mk ConNF.μ

There are exactly μ small subsets of any type α of size μ.

Small relations

One of the crucial differences between this formalisation and previous iterations of the paper is our extensive use of relational reasoning as opposed to function-based reasoning. This has some technical advantages that should hopefully become clear over the course of this work.

We will begin our study of relations by proving some smallness results for them, but we will first establish some terminology that will be used throughout this document.

The domain of a relation r is the set {a | ∃ b, r a b}. The codomain of r is the set {b | ∃ a, r a b}.

A relation r is called

• injective, if r a b and r a' b imply a = a';
• surjective, if for every b, there is some a such that r a b;
• coinjective, if r a b and r a b' imply b = b';
• cosurjective, if for every a, there is some b such that r a b;
• one-to-one, if r is both injective and coinjective;
• functional, if r is both coinjective and cosurjective (so is a set-theoretic function);
• cofunctional, if r is both injective and surjective (so is the converse of a set-theoretic function);
• bijective, if r is both functional and cofunctional;
• permutative, if r is one-to-one and its domain and codomain are equal.

The image of a set s under a relation r is the set {b | ∃ a ∈ s, r a b}. The graph of a relation r is the set {(a, b) | r a b}. We can now state our results.

theorem ConNF.image_small_of_coinjective [ConNF.Params] {α β : Type u} {r : Rel α β} (h : r.Coinjective) {s : Set α} (hs : ConNF.Small s) : ConNF.Small (r.image s)

The image of any small set under a coinjective relation is small. This is a generalisation of the fact that the image of a small set under a function (or functional relation) is small.

theorem ConNF.small_codom_of_small_dom [ConNF.Params] {α β : Type u} {r : Rel α β} (h : r.Coinjective) (h' : ConNF.Small r.dom) : ConNF.Small r.codom

If the domain of a coinjective relation is small, then its codomain is also small. This is a special case of the previous result.

theorem ConNF.small_graph' [ConNF.Params] {α β : Type u} {r : Rel α β} (h₁ : ConNF.Small r.dom) (h₂ : ConNF.Small r.codom) : ConNF.Small r.graph'

If the domain and codomain of a relation are small, then its graph is also small.

Nearness

Once we fix a notion of smallness, we can define an equivalence relation on sets of any type by declaring that two sets are near each other if their symmetric difference is small. This notion is used when defining near-litters, an important part of the ambient structure at the base type level.

def ConNF.Near [ConNF.Params] {α : Type u} (s t : Set α) : Prop

Two sets are called near if their symmetric difference is small.

Equations

• (s ~ t) = ConNF.Small (symmDiff s t)

We establish the symbol ~ to denote nearness.

def ConNF.«term_~_» : Lean.TrailingParserDescr

Two sets are called near if their symmetric difference is small.

Equations

• ConNF.«term_~_» = Lean.ParserDescr.trailingNode `ConNF.«term_~_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem ConNF.near_refl [ConNF.Params] {α : Type u} (s : Set α) : s ~ s

Nearness is reflexive.

theorem ConNF.near_rfl [ConNF.Params] {α : Type u} {s : Set α} : s ~ s

Like near_refl, but leaving all arguments implicit.

theorem ConNF.near_of_eq [ConNF.Params] {α : Type u} {s t : Set α} (h : s = t) : s ~ t

Equal sets are near.

theorem ConNF.near_symm [ConNF.Params] {α : Type u} {s t : Set α} (h : s ~ t) : t ~ s

Nearness is symmetric.

theorem ConNF.near_trans [ConNF.Params] {α : Type u} {s t u : Set α} (h₁ : s ~ t) (h₂ : t ~ u) : s ~ u

Nearness is transitive.

instance ConNF.instTransSetNear [ConNF.Params] {α : Type u} : Trans ConNF.Near ConNF.Near ConNF.Near

Equations

• ConNF.instTransSetNear = { trans := ⋯ }

theorem ConNF.near_symmDiff_self_of_small [ConNF.Params] {α : Type u} {s t : Set α} (h : ConNF.Small s) : symmDiff s t ~ t

If s is small, then s ∆ t is near t for any t.

theorem ConNF.near_union_of_small [ConNF.Params] {α : Type u} {s t : Set α} (h : ConNF.Small s) : t ∪ s ~ t

If s is small, then t ∪ s is near t for any t.

theorem ConNF.near_image [ConNF.Params] {α β : Type u} {s t : Set α} (h : s ~ t) (f : α → β) : f '' s ~ f '' t

Nearness is preserved under function application.

theorem ConNF.near_symmDiff_iff [ConNF.Params] {α : Type u} {s t : Set α} (u : Set α) : symmDiff u s ~ symmDiff u t ↔ s ~ t

Symmetric differences can be cancelled when comparing sets for nearness.

theorem ConNF.card_le_of_near [ConNF.Params] {α : Type u} {s t : Set α} (h₁ : s ~ t) (h₂ : ¬ConNF.Small t) : Cardinal.mk ↑t ≤ Cardinal.mk ↑s

theorem ConNF.card_eq_of_near [ConNF.Params] {α : Type u} {s t : Set α} (h₁ : s ~ t) (h₂ : ¬ConNF.Small t) : Cardinal.mk ↑s = Cardinal.mk ↑t

Two large sets that are near each other have the same cardinality (and we only need to suppose that one of them is large to draw this conclusion).

theorem ConNF.card_inter_of_near [ConNF.Params] {α : Type u} {s t : Set α} (h₁ : s ~ t) (h₂ : ¬ConNF.Small s) : Cardinal.mk ↑(s ∩ t) = Cardinal.mk ↑s

If s and t are large and near each other, then their intersection has the same cardinality as both s and t.

theorem ConNF.inter_nonempty_of_near [ConNF.Params] {α : Type u} {s t : Set α} (h₁ : s ~ t) (h₂ : ¬ConNF.Small s) : (s ∩ t).Nonempty

Any two large sets that are near each other must have nonempty intersection.

theorem ConNF.card_near_le [ConNF.Params] {α : Type u} (s : Set α) (h : Cardinal.mk α ≤ Cardinal.mk ConNF.μ) : Cardinal.mk ↑{t : Set α | t ~ s} ≤ Cardinal.mk ConNF.μ

If α is any type with cardinality bounded by μ, then the amount of sets near a given set s is also bounded by μ.

theorem ConNF.card_near_eq [ConNF.Params] {α : Type u} (s : Set α) (h : Cardinal.mk α = Cardinal.mk ConNF.μ) : Cardinal.mk ↑{t : Set α | t ~ s} = Cardinal.mk ConNF.μ

If α is any type with cardinality exactly μ, then the amount of sets near a given set s is precisely μ.