Enumerations

In this file, we define enumerations of a type.

Main declarations

• ConNF.Enumeration: The type family of enumerations.

structure ConNF.Enumeration [ConNF.Params] (X : Type u) : Type u

• bound : ConNF.κ
• rel : Rel ConNF.κ X
• lt_bound : ∀ i ∈ self.rel.dom, i < self.bound
• rel_coinjective : self.rel.Coinjective

theorem ConNF.Enumeration.ext {inst✝ : ConNF.Params} {X : Type u} {x y : ConNF.Enumeration X} (bound : x.bound = y.bound) (rel : x.rel = y.rel) : x = y

instance ConNF.Enumeration.instCoeTCSet [ConNF.Params] {X : Type u} : CoeTC (ConNF.Enumeration X) (Set X)

Equations

• ConNF.Enumeration.instCoeTCSet = { coe := fun (E : ConNF.Enumeration X) => E.rel.codom }

instance ConNF.Enumeration.instMembership [ConNF.Params] {X : Type u} : Membership X (ConNF.Enumeration X)

Equations

• ConNF.Enumeration.instMembership = { mem := fun (E : ConNF.Enumeration X) (x : X) => x ∈ E.rel.codom }

theorem ConNF.Enumeration.mem_iff [ConNF.Params] {X : Type u} (x : X) (E : ConNF.Enumeration X) : x ∈ E ↔ x ∈ E.rel.codom

theorem ConNF.Enumeration.mem_congr [ConNF.Params] {X : Type u} {E F : ConNF.Enumeration X} (h : E = F) (x : X) : x ∈ E ↔ x ∈ F

theorem ConNF.Enumeration.dom_small [ConNF.Params] {X : Type u} (E : ConNF.Enumeration X) : ConNF.Small E.rel.dom

theorem ConNF.Enumeration.coe_small [ConNF.Params] {X : Type u} (E : ConNF.Enumeration X) : ConNF.Small E.rel.codom

theorem ConNF.Enumeration.graph'_small [ConNF.Params] {X : Type u} (E : ConNF.Enumeration X) : ConNF.Small E.rel.graph'

noncomputable def ConNF.Enumeration.empty [ConNF.Params] {X : Type u} : ConNF.Enumeration X

Equations

• ConNF.Enumeration.empty = { bound := 0, rel := fun (x : ConNF.κ) (x : X) => False, lt_bound := ⋯, rel_coinjective := ⋯ }

@[simp]

theorem ConNF.Enumeration.not_mem_empty [ConNF.Params] {X : Type u} (x : X) : x ∉ ConNF.Enumeration.empty

noncomputable def ConNF.Enumeration.singleton [ConNF.Params] {X : Type u} (x : X) : ConNF.Enumeration X

Equations

• ConNF.Enumeration.singleton x = { bound := 1, rel := fun (i : ConNF.κ) (y : X) => i = 0 ∧ y = x, lt_bound := ⋯, rel_coinjective := ⋯ }

@[simp]

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

theorem ConNF.Enumeration.singleton_injective [ConNF.Params] {X : Type u} : Function.Injective ConNF.Enumeration.singleton

Cardinality bounds on enumerations

theorem ConNF.card_enumeration_ge [ConNF.Params] (X : Type u) : Cardinal.mk X ≤ Cardinal.mk (ConNF.Enumeration X)

def ConNF.enumerationEmbedding [ConNF.Params] (X : Type u) : ConNF.Enumeration X ↪ ConNF.κ × ↑{s : Set (ConNF.κ × X) | ConNF.Small s}

Equations

• ConNF.enumerationEmbedding X = { toFun := fun (E : ConNF.Enumeration X) => (E.bound, ⟨E.rel.graph', ⋯⟩), inj' := ⋯ }

theorem ConNF.card_enumeration_le [ConNF.Params] {X : Type u} (h : Cardinal.mk X ≤ Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.Enumeration X) ≤ Cardinal.mk ConNF.μ

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

theorem ConNF.card_enumeration_eq [ConNF.Params] {X : Type u} (h : Cardinal.mk X = Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.Enumeration X) = Cardinal.mk ConNF.μ

Enumerations from sets

theorem ConNF.Enumeration.exists_equiv [ConNF.Params] {X : Type u} (s : Set X) (hs : ConNF.Small s) : Nonempty ((i : ConNF.κ) × (↑s ≃ ↑(Set.Iio i)))

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

Equations

• ConNF.Enumeration.ofSet s hs = { bound := ⋯.some.fst, rel := fun (i : ConNF.κ) (x : X) => ∃ (h : x ∈ s), i = ↑(⋯.some.snd ⟨x, h⟩), lt_bound := ⋯, rel_coinjective := ⋯ }

@[simp]

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

@[simp]

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

Operations on enumerations

def ConNF.Enumeration.image [ConNF.Params] {X Y : Type u} (E : ConNF.Enumeration X) (f : X → Y) : ConNF.Enumeration Y

Equations

• E.image f = { bound := E.bound, rel := fun (i : ConNF.κ) (y : Y) => ∃ (x : X), E.rel i x ∧ f x = y, lt_bound := ⋯, rel_coinjective := ⋯ }

@[simp]

theorem ConNF.Enumeration.image_bound [ConNF.Params] {X Y : Type u} {E : ConNF.Enumeration X} {f : X → Y} : (E.image f).bound = E.bound

theorem ConNF.Enumeration.image_rel [ConNF.Params] {X Y : Type u} {E : ConNF.Enumeration X} {f : X → Y} (i : ConNF.κ) (y : Y) : (E.image f).rel i y ↔ ∃ (x : X), E.rel i x ∧ f x = y

@[simp]

theorem ConNF.Enumeration.mem_image [ConNF.Params] {X Y : Type u} {E : ConNF.Enumeration X} {f : X → Y} (y : Y) : y ∈ E.image f ↔ y ∈ f '' E.rel.codom

def ConNF.Enumeration.invImage [ConNF.Params] {X Y : Type u} (E : ConNF.Enumeration X) (f : Y → X) (hf : Function.Injective f) : ConNF.Enumeration Y

Equations

• E.invImage f hf = { bound := E.bound, rel := fun (i : ConNF.κ) (y : Y) => E.rel i (f y), lt_bound := ⋯, rel_coinjective := ⋯ }

theorem ConNF.Enumeration.invImage_rel [ConNF.Params] {X Y : Type u} {E : ConNF.Enumeration X} {f : Y → X} {hf : Function.Injective f} (i : ConNF.κ) (y : Y) : (E.invImage f hf).rel i y ↔ E.rel i (f y)

@[simp]

theorem ConNF.Enumeration.mem_invImage [ConNF.Params] {X Y : Type u} {E : ConNF.Enumeration X} {f : Y → X} {hf : Function.Injective f} (y : Y) : y ∈ E.invImage f hf ↔ f y ∈ E

def ConNF.Enumeration.comp [ConNF.Params] {X Y : Type u} (E : ConNF.Enumeration X) (r : Rel X Y) (hr : r.Coinjective) : ConNF.Enumeration Y

Equations

• E.comp r hr = { bound := E.bound, rel := E.rel.comp r, lt_bound := ⋯, rel_coinjective := ⋯ }

instance ConNF.Enumeration.instSMulOfMulAction [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] : SMul G (ConNF.Enumeration X)

Equations

• ConNF.Enumeration.instSMulOfMulAction = { smul := fun (π : G) (E : ConNF.Enumeration X) => E.invImage (fun (x : X) => π⁻¹ • x) ⋯ }

@[simp]

theorem ConNF.Enumeration.smul_rel [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : ConNF.Enumeration X) (i : ConNF.κ) (x : X) : (π • E).rel i x ↔ E.rel i (π⁻¹ • x)

@[simp]

theorem ConNF.Enumeration.mem_smul [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : ConNF.Enumeration X) (x : X) : x ∈ π • E ↔ π⁻¹ • x ∈ E

@[simp]

theorem ConNF.Enumeration.smul_rel_dom [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : ConNF.Enumeration X) : (π • E).rel.dom = E.rel.dom

@[simp]

theorem ConNF.Enumeration.smul_rel_codom [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : ConNF.Enumeration X) : (π • E).rel.codom = π • E.rel.codom

@[simp]

theorem ConNF.Enumeration.smul_coe [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : ConNF.Enumeration X) : (π • E).rel.codom = π • E.rel.codom

instance ConNF.Enumeration.instMulAction [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] : MulAction G (ConNF.Enumeration X)

Equations

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

theorem ConNF.Enumeration.mem_smul_iff [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (x : X) (g : G) (E : ConNF.Enumeration X) : x ∈ g • E ↔ g⁻¹ • x ∈ E

theorem ConNF.Enumeration.eq_of_smul_eq_smul [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] {g₁ g₂ : G} {E : ConNF.Enumeration X} (h : g₁ • E = g₂ • E) (x : X) (hx : x ∈ E) : g₁ • x = g₂ • x

theorem ConNF.Enumeration.eq_of_smul_eq [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] {g : G} {E : ConNF.Enumeration X} (h : g • E = E) (x : X) (hx : x ∈ E) : g • x = x

@[simp]

theorem ConNF.Enumeration.smul_singleton [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] {g : G} {x : X} : g • ConNF.Enumeration.singleton x = ConNF.Enumeration.singleton (g • x)

Concatenation of enumerations

noncomputable instance ConNF.Enumeration.instAdd [ConNF.Params] {X : Type u} : Add (ConNF.Enumeration X)

Equations

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

@[simp]

theorem ConNF.Enumeration.add_bound [ConNF.Params] {X : Type u} (E F : ConNF.Enumeration X) : (E + F).bound = E.bound + F.bound

theorem ConNF.Enumeration.rel_add_iff [ConNF.Params] {X : Type u} {E F : ConNF.Enumeration X} (i : ConNF.κ) (x : X) : (E + F).rel i x ↔ E.rel i x ∨ ∃ (j : ConNF.κ), E.bound + j = i ∧ F.rel j x

theorem ConNF.Enumeration.add_rel_dom [ConNF.Params] {X : Type u} (E F : ConNF.Enumeration X) : (E + F).rel.dom = E.rel.dom ∪ (fun (x : ConNF.κ) => E.bound + x) '' F.rel.dom

@[simp]

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

@[simp]

theorem ConNF.Enumeration.coe_add [ConNF.Params] {X : Type u} {E F : ConNF.Enumeration X} : (E + F).rel.codom = E.rel.codom ∪ F.rel.codom

@[simp]

theorem ConNF.Enumeration.add_empty [ConNF.Params] {X : Type u} (E : ConNF.Enumeration X) : E + ConNF.Enumeration.empty = E

theorem ConNF.Enumeration.add_inj_of_bound_eq_bound [ConNF.Params] {X : Type u} {E F G H : ConNF.Enumeration X} (h : E.bound = F.bound) (h' : E + G = F + H) : E = F ∧ G = H

theorem ConNF.Enumeration.add_inj_iff_of_bound_eq_bound [ConNF.Params] {X : Type u} {E F G H : ConNF.Enumeration X} (h : E.bound = F.bound) : E + G = F + H ↔ E = F ∧ G = H

theorem ConNF.Enumeration.smul_add [ConNF.Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (g : G) (E F : ConNF.Enumeration X) : g • (E + F) = g • E + g • F