Smallness

In this file, we define what it means for a set to be small.

Main declarations

• ConNF.Small: A set is small if its cardinality (as a type) is strictly less than κ.
• ConNF.IsNear: 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 strictly 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.Set.Subsingleton.small [ConNF.Params] {α : Type u} {s : Set α} (hs : 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_setOf [ConNF.Params] {α : Type u} (p : α → Prop) : (ConNF.Small fun (a : α) => p a) ↔ ConNF.Small {a : α | p a}

theorem ConNF.small_of_forall_not_mem [ConNF.Params] {α : Type u} {s : Set α} (h : ∀ (x : α), x ∉ s) : ConNF.Small s

theorem ConNF.Small.mono [ConNF.Params] {α : Type u} {s : Set α} {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.union [ConNF.Params] {α : Type u} {s : Set α} {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 : Set α} {t : Set α} (hs : ConNF.Small s) (ht : ConNF.Small t) : ConNF.Small (symmDiff s t)

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

theorem ConNF.small_iUnion [ConNF.Params] {ι : Type u} {α : 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.bUnion [ConNF.Params] {ι : Type u} {α : 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} {β : Type u} {f : α → β} {s : Set α} : 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} {β : Type u} {f : α → β} {s : Set β} (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.Small.image_subset [ConNF.Params] {α : Type u} {β : Type u} {s : Set α} {t : Set β} (f : α → β) (h : Function.Injective f) : ConNF.Small t → f '' s ⊆ t → ConNF.Small s

A set is small if its image under an injective function is contained in a small set.

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

Nearness

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

Two sets are near if their symmetric difference is small.

Equations

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

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

A set is near itself.

theorem ConNF.isNear_rfl [ConNF.Params] {α : Type u} {s : Set α} : ConNF.IsNear s s

A version of the is_near_refl lemma that does not require the set s to be given explicitly. The value of s will be inferred automatically by the elaborator.

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

If s is near t, then t is near s.

theorem ConNF.isNear_comm [ConNF.Params] {α : Type u} {s : Set α} {t : Set α} : ConNF.IsNear s t ↔ ConNF.IsNear t s

s is near t if and only if t is near s. In each direction, this is an application of the is_near.symm lemma. Lemmas using ↔ can be used with rw, so this form of the result is particularly useful.

theorem ConNF.IsNear.trans [ConNF.Params] {α : Type u} {s : Set α} {t : Set α} {u : Set α} (hst : ConNF.IsNear s t) (htu : ConNF.IsNear t u) : ConNF.IsNear s u

Nearness is transitive: if s is near t and t is near u, then s is near u.

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

If two sets are near each other, then their images under an arbitrary function are also near.

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

theorem ConNF.Small.isNear_iff [ConNF.Params] {α : Type u} {s : Set α} {t : Set α} (hs : ConNF.Small s) : ConNF.Small t ↔ ConNF.IsNear s t

theorem ConNF.IsNear.κ_le [ConNF.Params] {α : Type u} {s : Set α} {t : Set α} (h : ConNF.IsNear s t) (hs : Cardinal.mk ConNF.κ ≤ Cardinal.mk ↑s) : Cardinal.mk ConNF.κ ≤ Cardinal.mk ↑t

theorem ConNF.IsNear.mk_inter [ConNF.Params] {α : Type u} {s : Set α} {t : Set α} (h : ConNF.IsNear s t) (hs : Cardinal.mk ConNF.κ ≤ Cardinal.mk ↑s) : Cardinal.mk ConNF.κ ≤ Cardinal.mk ↑(s ∩ t)