Enumerations

In this file, we define sequences indexed by "small ordinals", which here is taken to mean some inhabitant of κ.

Main declarations

• ConNF.Enumeration: The type of enumerations.
• ConNF.mk_enumeration and ConNF.mk_enumeration_le: Bounds on the size of the type of enumerations.

theorem ConNF.Enumeration.ext_iff : ∀ {inst : ConNF.Params} {α : Type u_1} (x y : ConNF.Enumeration α), x = y ↔ x.max = y.max ∧ HEq x.f y.f

theorem ConNF.Enumeration.ext : ∀ {inst : ConNF.Params} {α : Type u_1} (x y : ConNF.Enumeration α), x.max = y.max → HEq x.f y.f → x = y

structure ConNF.Enumeration [ConNF.Params] (α : Type u_1) : Type (max u u_1)

An α-enumeration is a function from a proper initial segment of κ to α.

• max : ConNF.κ
• f : (i : ConNF.κ) → i < self.max → α

theorem ConNF.Enumeration.ext' [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} (h : E.max = F.max) (h' : ∀ (i : ConNF.κ) (hE : i < E.max) (hF : i < F.max), E.f i hE = F.f i hF) : E = F

The main induction principle for enumerations. This statement of extensionality avoids dealing with heterogeneous equality.

def ConNF.Enumeration.carrier [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) : Set α

The range of an enumeration. We say that some inhabitant of α is "in" an enumeration E if it is an element of the carrier.

Equations

• E.carrier = {c : α | ∃ (i : ConNF.κ) (h : i < E.max), c = E.f i h}

instance ConNF.instCoeTCEnumerationSet [ConNF.Params] {α : Type u_1} : CoeTC (ConNF.Enumeration α) (Set α)

Equations

• ConNF.instCoeTCEnumerationSet = { coe := fun (E : ConNF.Enumeration α) => E.carrier }

instance ConNF.instMembershipEnumeration [ConNF.Params] {α : Type u_1} : Membership α (ConNF.Enumeration α)

Equations

• ConNF.instMembershipEnumeration = { mem := fun (x : α) (E : ConNF.Enumeration α) => x ∈ E.carrier }

theorem ConNF.Enumeration.mem_carrier_iff [ConNF.Params] {α : Type u_1} (x : α) (E : ConNF.Enumeration α) : x ∈ E.carrier ↔ ∃ (i : ConNF.κ) (h : i < E.max), x = E.f i h

theorem ConNF.Enumeration.mem_iff [ConNF.Params] {α : Type u_1} (c : α) (E : ConNF.Enumeration α) : c ∈ E ↔ ∃ (i : ConNF.κ) (h : i < E.max), c = E.f i h

theorem ConNF.Enumeration.f_mem [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (i : ConNF.κ) (hi : i < E.max) : E.f i hi ∈ E

theorem ConNF.Enumeration.carrier_small [ConNF.Params] {α : Type u} (E : ConNF.Enumeration α) : ConNF.Small E.carrier

theorem ConNF.Enumeration.small [ConNF.Params] {α : Type u} (E : ConNF.Enumeration α) : ConNF.Small E.carrier

Enumerations give rise to small sets.

def ConNF.Enumeration.singleton [ConNF.Params] {α : Type u_1} (x : α) : ConNF.Enumeration α

Equations

• ConNF.Enumeration.singleton x = { max := 1, f := fun (x_1 : ConNF.κ) (x_2 : x_1 < 1) => x }

@[simp]

theorem ConNF.Enumeration.mem_singleton_iff [ConNF.Params] {α : Type u_1} (x : α) (y : α) : y ∈ ConNF.Enumeration.singleton x ↔ y = x

@[simp]

theorem ConNF.Enumeration.singleton_carrier [ConNF.Params] {α : Type u_1} (x : α) : (ConNF.Enumeration.singleton x).carrier = {x}

@[simp]

theorem ConNF.Enumeration.singleton_coe [ConNF.Params] {α : Type u_1} (x : α) : (ConNF.Enumeration.singleton x).carrier = {x}

@[simp]

theorem ConNF.Enumeration.singleton_f [ConNF.Params] {α : Type u_1} (x : α) (i : ConNF.κ) (hi : i < (ConNF.Enumeration.singleton x).max) : (ConNF.Enumeration.singleton x).f i hi = x

Counting enumerations

We now establish that there are precisely μ enumerations taking values in α, given that α has size μ. This requires a technical lemma about cardinal arithmetic, given in mk_fun_le.

def ConNF.enumerationEquiv [ConNF.Params] {α : Type u_1} : ConNF.Enumeration α ≃ (max : ConNF.κ) × (↑(Set.Iio max) → α)

Equations

• One or more equations did not get rendered due to their size.

def ConNF.funMap (α : Type u_1) (β : Type u_1) [LT β] (f : α → β) : { E : Set β // Cardinal.mk ↑E ≤ Cardinal.mk α } × (α → α → Prop)

Equations

• ConNF.funMap α β f = (⟨Set.range f, ⋯⟩, InvImage (fun (x x_1 : β) => x < x_1) f)

theorem ConNF.funMap_injective {α : Type u_1} {β : Type u_1} [LinearOrder β] [IsWellOrder β fun (x x_1 : β) => x < x_1] : Function.Injective (ConNF.funMap α β)

Suppose that β is well-ordered. Then, a function f : α → β is uniquely determined by its range together with the inverse image of the < relation under f.

theorem ConNF.mk_fun_le {α : Type u} {β : Type u} : Cardinal.mk (α → β) ≤ Cardinal.mk ({ E : Set β // Cardinal.mk ↑E ≤ Cardinal.mk α } × (α → α → Prop))

The amount of functions α → β is bounded by the amount of subsets of β of size at most α, multiplied by the amount of relations on α. We prove this by giving β an arbitrary well-ordering and using funMap_injective.

theorem ConNF.pow_le_of_isStrongLimit' {α : Type u} {β : Type u} [Infinite α] [Infinite β] (h₁ : (Cardinal.mk β).IsStrongLimit) (h₂ : Cardinal.mk α < (Cardinal.mk β).ord.cof) : Cardinal.mk β ^ Cardinal.mk α ≤ Cardinal.mk β

theorem ConNF.pow_lt_of_isStrongLimit' {α : Type u} {β : Type u} {γ : Type u} [Infinite β] (hα : Cardinal.mk α < Cardinal.mk γ) (hβ : Cardinal.mk β < Cardinal.mk γ) (hγ : (Cardinal.mk γ).IsStrongLimit) : Cardinal.mk α ^ Cardinal.mk β < Cardinal.mk γ

theorem ConNF.pow_le_of_isStrongLimit {κ : Cardinal.{u}} {μ : Cardinal.{u}} (h₁ : μ.IsStrongLimit) (h₂ : κ < μ.ord.cof) : μ ^ κ ≤ μ

If μ is a strong limit cardinal and κ is less than the cofinality of μ, then μ ^ κ ≤ μ. This is a partial converse to a certain form of König's theorem (Cardinal.lt_power_cof), which implies that μ < μ ^ κ if κ is at least the cofinality of μ.

theorem ConNF.pow_lt_of_isStrongLimit {ξ : Cardinal.{u}} {κ : Cardinal.{u}} {μ : Cardinal.{u}} (hξ : ξ < μ) (hκ : κ < μ) (hμ : μ.IsStrongLimit) : ξ ^ κ < μ

Strong limits are closed under exponentials.

theorem ConNF.mk_enumeration [ConNF.Params] {α : Type u} (mk_α : Cardinal.mk α = Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.Enumeration α) = Cardinal.mk ConNF.μ

Given that #α = #μ, there are exactly μ enumerations.

theorem Cardinal.pow_mono_left (a : Cardinal.{u_1}) (ha : a ≠ 0) : Monotone fun (b : Cardinal.{u_1}) => a ^ b

theorem ConNF.max_eq_zero [ConNF.Params] {α : Type u_1} [IsEmpty α] (E : ConNF.Enumeration α) : E.max = 0

instance ConNF.instSubsingletonEnumerationOfIsEmpty [ConNF.Params] {α : Type u_1} [IsEmpty α] : Subsingleton (ConNF.Enumeration α)

Equations

• ⋯ = ⋯

theorem Cardinal.mul_le_of_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (ha : a ≤ c) (hb : b ≤ c) (hc : Cardinal.aleph0 ≤ c) : a * b ≤ c

theorem Cardinal.lt_pow {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : 1 < a) : b < a ^ b

theorem ConNF.mk_enumeration_ne_zero [ConNF.Params] {α : Type u} : Cardinal.mk (ConNF.Enumeration α) ≠ 0

theorem ConNF.mk_enumeration_le [ConNF.Params] {α : Type u} [Nontrivial α] : Cardinal.mk (ConNF.Enumeration α) ≤ Cardinal.mk α ^ Cardinal.mk ConNF.κ

A bound on the amount of enumerations.

theorem ConNF.mk_enumeration_le_of_subsingleton [ConNF.Params] {α : Type u} [Subsingleton α] : Cardinal.mk (ConNF.Enumeration α) ≤ Cardinal.mk ConNF.κ

theorem ConNF.mk_enumeration_lt [ConNF.Params] {α : Type u} (h : Cardinal.mk α < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.Enumeration α) < Cardinal.mk ConNF.μ

A bound on the amount of enumerations.

Operations on enumerations

def ConNF.Enumeration.image [ConNF.Params] {α : Type u_1} {β : Type u_2} (E : ConNF.Enumeration α) (f : α → β) : ConNF.Enumeration β

The image of an enumeration under a function.

Equations

• E.image f = { max := E.max, f := fun (i : ConNF.κ) (hi : i < E.max) => f (E.f i hi) }

@[simp]

theorem ConNF.Enumeration.image_max [ConNF.Params] {α : Type u_1} {β : Type u_2} (E : ConNF.Enumeration α) (f : α → β) : (E.image f).max = E.max

@[simp]

theorem ConNF.Enumeration.image_f [ConNF.Params] {α : Type u_1} {β : Type u_2} (E : ConNF.Enumeration α) (f : α → β) (i : ConNF.κ) (hi : i < E.max) : (E.image f).f i hi = f (E.f i hi)

@[simp]

theorem ConNF.Enumeration.image_carrier [ConNF.Params] {α : Type u_1} {β : Type u_2} (E : ConNF.Enumeration α) (f : α → β) : (E.image f).carrier = f '' E.carrier

@[simp]

theorem ConNF.Enumeration.image_coe [ConNF.Params] {α : Type u_1} {β : Type u_2} (E : ConNF.Enumeration α) (f : α → β) : (E.image f).carrier = f '' E.carrier

theorem ConNF.Enumeration.apply_mem_image [ConNF.Params] {α : Type u_1} {β : Type u_2} {E : ConNF.Enumeration α} {x : α} (h : x ∈ E) (f : α → β) : f x ∈ E.image f

theorem ConNF.Enumeration.apply_eq_of_image_eq [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} (f : α → α) (hE : E.image f = E) {x : α} (hx : x ∈ E) : f x = x

instance ConNF.Enumeration.instSMul [ConNF.Params] {α : Type u_1} {G : Type u_2} [SMul G α] : SMul G (ConNF.Enumeration α)

The pointwise image of an enumeration under a group action (or similar).

Equations

• ConNF.Enumeration.instSMul = { smul := fun (g : G) (E : ConNF.Enumeration α) => E.image fun (x : α) => g • x }

@[simp]

theorem ConNF.Enumeration.smul_max [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] (g : G) (E : ConNF.Enumeration α) : (g • E).max = E.max

@[simp]

theorem ConNF.Enumeration.smul_f [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] (g : G) (E : ConNF.Enumeration α) (i : ConNF.κ) (hi : i < E.max) : (g • E).f i hi = g • E.f i hi

@[simp]

theorem ConNF.Enumeration.smul_carrier [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] (g : G) (E : ConNF.Enumeration α) : (g • E).carrier = g • E.carrier

@[simp]

theorem ConNF.Enumeration.smul_coe [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] (g : G) (E : ConNF.Enumeration α) : (g • E).carrier = g • E.carrier

theorem ConNF.Enumeration.smul_mem_smul [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] {E : ConNF.Enumeration α} {x : α} (h : x ∈ E) (g : G) : g • x ∈ g • E

theorem ConNF.Enumeration.smul_eq_of_smul_eq [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] {g : G} {E : ConNF.Enumeration α} (hE : g • E = E) {x : α} (hx : x ∈ E) : g • x = x

instance ConNF.Enumeration.instMulAction [ConNF.Params] {α : Type u_1} {G : Type u_2} [Monoid G] [MulAction G α] : MulAction G (ConNF.Enumeration α)

Any group that acts on α also acts on α-valued enumerations pointwise.

Equations

• ConNF.Enumeration.instMulAction = MulAction.mk ⋯ ⋯

theorem ConNF.Enumeration.smul_mem_smul_iff [ConNF.Params] {α : Type u_2} {G : Type u_1} [Group G] [MulAction G α] {E : ConNF.Enumeration α} {x : α} (g : G) : g • x ∈ g • E ↔ x ∈ E

instance ConNF.Enumeration.instAdd [ConNF.Params] {α : Type u_1} : Add (ConNF.Enumeration α)

The concatenation of two enumerations.

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Enumeration.add_f_eq [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {i : ConNF.κ} (hi : i < (E + F).max) : (E + F).f i hi = if hi' : i < E.max then E.f i hi' else F.f (i - E.max) ⋯

@[simp]

theorem ConNF.Enumeration.add_max [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} : (E + F).max = E.max + F.max

theorem ConNF.Enumeration.add_f_left [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {i : ConNF.κ} (h : i < E.max) : (E + F).f i ⋯ = E.f i h

theorem ConNF.Enumeration.add_f_right [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {i : ConNF.κ} (h₁ : i < (E + F).max) (h₂ : E.max ≤ i) : (E + F).f i h₁ = F.f (i - E.max) ⋯

theorem ConNF.Enumeration.add_f_right_add [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {i : ConNF.κ} (h : i < F.max) : (E + F).f (E.max + i) ⋯ = F.f i h

theorem ConNF.Enumeration.add_coe [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) : (E + F).carrier = E.carrier ∪ F.carrier

@[simp]

theorem ConNF.Enumeration.mem_add_iff [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) (x : α) : x ∈ E + F ↔ x ∈ E ∨ x ∈ F

theorem ConNF.Enumeration.add_congr [ConNF.Params] {α : Type u_1} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {G : ConNF.Enumeration α} {H : ConNF.Enumeration α} (hEF : E.max = F.max) (h : E + G = F + H) : E = F ∧ G = H

@[simp]

theorem ConNF.Enumeration.smul_add [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] {g : G} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) : g • (E + F) = g • E + g • F

Group actions distribute over sums of enumerations.

The partial order on enumerations

We say that E ≤ F when F has larger domain than E and agrees on the smaller domain.

instance ConNF.Enumeration.instLE [ConNF.Params] {α : Type u_1} : LE (ConNF.Enumeration α)

Equations

• ConNF.Enumeration.instLE = { le := fun (E F : ConNF.Enumeration α) => E.max ≤ F.max ∧ ∀ (i : ConNF.κ) (hE : i < E.max) (hF : i < F.max), E.f i hE = F.f i hF }

instance ConNF.Enumeration.instLT [ConNF.Params] {α : Type u_1} : LT (ConNF.Enumeration α)

Equations

• ConNF.Enumeration.instLT = { lt := fun (E F : ConNF.Enumeration α) => E.max < F.max ∧ ∀ (i : ConNF.κ) (hE : i < E.max) (hF : i < F.max), E.f i hE = F.f i hF }

theorem ConNF.Enumeration.le_iff [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) : E ≤ F ↔ E.max ≤ F.max ∧ ∀ (i : ConNF.κ) (hE : i < E.max) (hF : i < F.max), E.f i hE = F.f i hF

theorem ConNF.Enumeration.lt_iff [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) : E < F ↔ E.max < F.max ∧ ∀ (i : ConNF.κ) (hE : i < E.max) (hF : i < F.max), E.f i hE = F.f i hF

instance ConNF.Enumeration.instPartialOrder [ConNF.Params] {α : Type u_1} : PartialOrder (ConNF.Enumeration α)

Equations

• ConNF.Enumeration.instPartialOrder = PartialOrder.mk ⋯

theorem ConNF.Enumeration.image_le_image [ConNF.Params] {α : Type u_1} {β : Type u_2} {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} (h : E ≤ F) (f : α → β) : E.image f ≤ F.image f

theorem ConNF.Enumeration.smul_le_smul [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} (h : E ≤ F) (g : G) : g • E ≤ g • F

theorem ConNF.Enumeration.le_inv_iff_smul_le [ConNF.Params] {α : Type u_2} {G : Type u_1} [Group G] [MulAction G α] {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} (g : G) : E ≤ g⁻¹ • F ↔ g • E ≤ F

theorem ConNF.Enumeration.eq_of_le [ConNF.Params] {α : Type u_2} {G : Type u_1} [SMul G α] {E : ConNF.Enumeration α} {F : ConNF.Enumeration α} {g : G} (h₁ : g • E ≤ F) (h₂ : E ≤ F) : g • E = E

theorem ConNF.Enumeration.le_add [ConNF.Params] {α : Type u_1} (E : ConNF.Enumeration α) (F : ConNF.Enumeration α) : E ≤ E + F

Converting sets to enumerations

We describe a procedure to produce an enumeration whose carrier is any given small set.

theorem ConNF.Enumeration.ord_lt_of_small [ConNF.Params] {α : Type u} {s : Set α} (hs : ConNF.Small s) [LinearOrder ↑s] [IsWellOrder ↑s fun (x x_1 : ↑s) => x < x_1] : (Ordinal.type fun (x x_1 : ↑s) => x < x_1) < Ordinal.type fun (x x_1 : ConNF.κ) => x < x_1

theorem ConNF.Enumeration.typein_lt_type_of_small [ConNF.Params] {α : Type u} {s : Set α} (hs : ConNF.Small s) [LinearOrder ↑s] [IsWellOrder ↑s fun (x x_1 : ↑s) => x < x_1] {i : ConNF.κ} (hi : i < Ordinal.enum (fun (x x_1 : ConNF.κ) => x < x_1) (Ordinal.type fun (x x_1 : ↑s) => x < x_1) ⋯) : Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i < Ordinal.type fun (x x_1 : ↑s) => x < x_1

def ConNF.Enumeration.ofSet' [ConNF.Params] {α : Type u} (s : Set α) (hs : ConNF.Small s) [LinearOrder ↑s] [IsWellOrder ↑s fun (x x_1 : ↑s) => x < x_1] : ConNF.Enumeration α

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConNF.Enumeration.ofSet'_coe [ConNF.Params] {α : Type u} (s : Set α) (hs : ConNF.Small s) [LinearOrder ↑s] [IsWellOrder ↑s fun (x x_1 : ↑s) => x < x_1] : (ConNF.Enumeration.ofSet' s hs).carrier = s

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

Converts a small set s into an enumeration with carrier set s.

Equations

• ConNF.Enumeration.ofSet s hs = ConNF.Enumeration.ofSet' s hs

@[simp]

theorem ConNF.Enumeration.ofSet_coe [ConNF.Params] {α : Type u} (s : Set α) (hs : ConNF.Small s) : (ConNF.Enumeration.ofSet s hs).carrier = s

@[simp]

theorem ConNF.Enumeration.mem_ofSet_iff [ConNF.Params] {α : Type u} (s : Set α) (hs : ConNF.Small s) (x : α) : x ∈ ConNF.Enumeration.ofSet s hs ↔ x ∈ s