Smallness

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

Main declarations

• ConNF.Small: A set is small if its cardinality is less than #κ.
• ConNF.Near: Two sets are near if their symmetric difference is small.

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

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

@[simp]

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

@[simp]

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

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

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

Unions of small subsets 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)

Unions of small subsets are small.

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)

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)

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)

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

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

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

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 α 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.μ

There are at most μ small sets 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 sets of a type of size μ.

Small relations

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)

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

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

Nearness

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)

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

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

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

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

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

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

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

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

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

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

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

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.μ

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.μ