def Finpartition.finsetImage {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : Finset α} (P : Finpartition a) (f : α → β) (hf : Function.Injective f) : Finpartition (Finset.image f a)

Equations

• P.finsetImage f hf = { parts := Finset.image (Finset.image f) P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

@[simp]

theorem Finpartition.finsetImage_parts {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {a : Finset α} (P : Finpartition a) (f : α → β) (hf : Function.Injective f) : (P.finsetImage f hf).parts = Finset.image (Finset.image f) P.parts

def Finpartition.extend' {α : Type u_1} [DecidableEq α] [DistribLattice α] [OrderBot α] {a b c : α} (P : Finpartition a) (hab : Disjoint a b) (hc : a ⊔ b = c) : Finpartition c

Equations

• P.extend' hab hc = if hb : b = ⊥ then P.copy ⋯ else P.extend hb hab hc

def Finpartition.modPartitions (s d : ℕ) (hd : d ≠ 0) (h : d ≤ s) : Finpartition (Finset.range s)

Equations

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

theorem Finpartition.modPartitions_parts_eq (s d : ℕ) (hd : d ≠ 0) (h : d ≤ s) : (Finpartition.modPartitions s d hd h).parts = Finset.image (fun (i : ℕ) => Finset.image (fun (x : ℕ) => i + d * x) (Finset.range ((s - i - 1) / d + 1))) (Finset.range d)