Documentation

ConNF.ModelData.Enumeration

Enumerations #

In this file, we define enumerations of a type.

Main declarations #

ConNF.Enumeration: The type family of enumerations.

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

bound : κ
rel : Rel κ X
lt_bound (i : κ) : i ∈ self.rel.dom → i < self.bound
rel_coinjective : self.rel.Coinjective

Instances For

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

x = y

instance ConNF.Enumeration.instCoeTCSet [Params] {X : Type u} :

CoeTC (Enumeration X) (Set X)

Equations

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

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

Membership X (Enumeration X)

Equations

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

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

x ∈ E ↔ x ∈ E.rel.codom

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

x ∈ E ↔ x ∈ F

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

Small E.rel.dom

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

Small E.rel.codom

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

Small E.rel.graph'

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

Equations

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

Instances For

@[simp]

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

x ∉ empty

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

Equations

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

Instances For

@[simp]

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

y ∈ singleton x ↔ y = x

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

Function.Injective singleton

Cardinality bounds on enumerations #

theorem ConNF.card_enumeration_ge [Params] (X : Type u) :

Cardinal.mk X ≤ Cardinal.mk (Enumeration X)

def ConNF.enumerationEmbedding [Params] (X : Type u) :

Enumeration X ↪ κ × ↑{s : Set (κ × X) | Small s}

Equations

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

Instances For

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

Cardinal.mk (Enumeration X) ≤ Cardinal.mk μ

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

Cardinal.mk (Enumeration X) < Cardinal.mk μ

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

Cardinal.mk (Enumeration X) = Cardinal.mk μ

Enumerations from sets #

theorem ConNF.Enumeration.exists_equiv [Params] {X : Type u} (s : Set X) (hs : Small s) :

Nonempty ((i : κ) × (↑s ≃ ↑(Set.Iio i)))

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

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 := ⋯ }

Instances For

@[simp]

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

x ∈ ofSet s hs ↔ x ∈ s

@[simp]

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

(ofSet s hs).rel.codom = s

Operations on enumerations #

def ConNF.Enumeration.image [Params] {X Y : Type u} (E : Enumeration X) (f : X → 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 := ⋯ }

Instances For

@[simp]

theorem ConNF.Enumeration.image_bound [Params] {X Y : Type u} {E : Enumeration X} {f : X → Y} :

(E.image f).bound = E.bound

theorem ConNF.Enumeration.image_rel [Params] {X Y : Type u} {E : Enumeration X} {f : X → Y} (i : κ) (y : Y) :

(E.image f).rel i y ↔ ∃ (x : X), E.rel i x ∧ f x = y

@[simp]

theorem ConNF.Enumeration.mem_image [Params] {X Y : Type u} {E : Enumeration X} {f : X → Y} (y : Y) :

y ∈ E.image f ↔ y ∈ f '' E.rel.codom

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

Equations

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

Instances For

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

(E.invImage f hf).rel i y ↔ E.rel i (f y)

@[simp]

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

y ∈ E.invImage f hf ↔ f y ∈ E

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

Equations

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

Instances For

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

SMul G (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 [Params] {G : Type u_1} {X : Type u} [Group G] [MulAction G X] (π : G) (E : Enumeration X) (i : κ) (x : X) :

(π • E).rel i x ↔ E.rel i (π⁻¹ • x)

@[simp]

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

x ∈ π • E ↔ π⁻¹ • x ∈ E

@[simp]

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

(π • E).rel.dom = E.rel.dom

@[simp]

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

(π • E).rel.codom = π • E.rel.codom

@[simp]

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

(π • E).rel.codom = π • E.rel.codom

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

MulAction G (Enumeration X)

Equations

ConNF.Enumeration.instMulAction = MulAction.mk ⋯ ⋯

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

x ∈ g • E ↔ g⁻¹ • x ∈ E

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

g₁ • x = g₂ • x

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

g • x = x

@[simp]

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

g • singleton x = singleton (g • x)

Concatenation of enumerations #

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

Add (Enumeration X)

Equations

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

@[simp]

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

(E + F).bound = E.bound + F.bound

theorem ConNF.Enumeration.rel_add_iff [Params] {X : Type u} {E F : Enumeration X} (i : κ) (x : X) :

(E + F).rel i x ↔ E.rel i x ∨ ∃ (j : κ), E.bound + j = i ∧ F.rel j x

theorem ConNF.Enumeration.add_rel_dom [Params] {X : Type u} (E F : Enumeration X) :

(E + F).rel.dom = E.rel.dom ∪ (fun (x : κ) => E.bound + x) '' F.rel.dom

@[simp]

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

x ∈ E + F ↔ x ∈ E ∨ x ∈ F

@[simp]

theorem ConNF.Enumeration.coe_add [Params] {X : Type u} {E F : Enumeration X} :

(E + F).rel.codom = E.rel.codom ∪ F.rel.codom

@[simp]

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

theorem ConNF.Enumeration.add_inj_of_bound_eq_bound [Params] {X : Type u} {E F G H : 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 [Params] {X : Type u} {E F G H : Enumeration X} (h : E.bound = F.bound) :

E + G = F + H ↔ E = F ∧ G = H

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

g • (E + F) = g • E + g • F