def Combinatorics.Partitions.FittingPartition (α : Type u_1) [Finite α] (k : Nat) (x : Nat → Nat) : Set (↥(Set.Iio k) → Set α)

Equations

• Combinatorics.Partitions.FittingPartition α k x = {y : ↥(Set.Iio k) → Set α | Set.IsPartition y ∧ ∀ (i : Nat) (h : i ∈ Set.Iio k), (Finite.ftype ↥(y ⟨i, h⟩)).cardinality = x i}

def Combinatorics.Partitions.FittingPartition.image_bij {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} (h : Function.Bijection α α) (y : ↥(Combinatorics.Partitions.FittingPartition α k x)) : ↥(Combinatorics.Partitions.FittingPartition α k x)

Equations

• Combinatorics.Partitions.FittingPartition.image_bij h y = ⟨fun (i : ↥(Set.Iio k)) => h.val '' y.val i, ⋯⟩

@[simp]

theorem Combinatorics.Partitions.FittingPartition.image_bij_takes_value {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} {h : Function.Bijection α α} {y z : ↥(Combinatorics.Partitions.FittingPartition α k x)} : Combinatorics.Partitions.FittingPartition.image_bij h y = z ↔ ∀ (i : ↥(Set.Iio k)), ∃ (h' : Function.Bijection ↥(y.val i) ↥(z.val i)), ∀ (x_1 : ↥(y.val i)), (h'.val x_1).val = h.val x_1.val

noncomputable def Combinatorics.Partitions.FittingPartition.preimage_to_bijections {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} {y z : ↥(Combinatorics.Partitions.FittingPartition α k x)} : Function.Bijection (↥{f : Function.Bijection α α | ∀ (i : ↥(Set.Iio k)), ∃ (h' : Function.Bijection ↥(y.val i) ↥(z.val i)), ∀ (x_2 : ↥(y.val i)), (h'.val x_2).val = f.val x_2.val}) ((i : ↥(Set.Iio k)) → Function.Bijection ↥(y.val i) ↥(z.val i))

Equations

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

theorem Combinatorics.Partitions.fittingPartition_nonempty {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} (hsum : Nat.sum_ft 0 k x = (Finite.ftype α).cardinality) : (Combinatorics.Partitions.FittingPartition α k x).Nonempty

instance instFiniteSubtypeForallNatMemSetIioFittingPartition {α : Type} {k : Nat} {x : Nat → Nat} [Finite α] : Finite ↥(Combinatorics.Partitions.FittingPartition α k x)

Equations

• ⋯ = ⋯

theorem Combinatorics.Partitions.cardinality_partitions' {α : Type} [Finite α] {k n : Nat} {x : Nat → Nat} (hn : (Finite.ftype α).cardinality = n) (hsum : Nat.sum_ft 0 k x = n) : ((Finite.ftype ↥(Combinatorics.Partitions.FittingPartition α k x)).cardinality * Nat.prod_ft 0 k fun (i : Nat) => (x i).factorial) = n.factorial

theorem Combinatorics.Partitions.cardinality_partitions {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} (hn : (Finite.ftype α).cardinality = Nat.sum_ft 0 k x) : ((Finite.ftype ↥(Combinatorics.Partitions.FittingPartition α k x)).cardinality * Nat.prod_ft 0 k fun (i : Nat) => (x i).factorial) = (Finite.ftype α).cardinality.factorial

theorem Combinatorics.Partitions.cardinality_partitions_div {α : Type} [Finite α] {k : Nat} {x : Nat → Nat} (hn : (Finite.ftype α).cardinality = Nat.sum_ft 0 k x) : (Finite.ftype ↥(Combinatorics.Partitions.FittingPartition α k x)).cardinality = (Finite.ftype α).cardinality.factorial / Nat.prod_ft 0 k fun (i : Nat) => (x i).factorial

noncomputable def Combinatorics.Partitions.FittingPartition.val_1_eq_compl_0_of_2 {α : Type} [Finite α] {x : ↥(Set.Iio 2) → Set α} (h : Set.IsPartition x) : x ⟨1, ⋯⟩ = (x ⟨0, ⋯⟩)ᶜ

Equations

• ⋯ = ⋯

noncomputable def Combinatorics.Partitions.FittingPartition.subset_as {α : Type} [Finite α] {k : Nat} : Function.Bijection ↥(Combinatorics.Partitions.FittingPartition α 2 fun (i : Nat) => if i = 0 then k else (Finite.ftype α).cardinality - k) ↥{a : Set α | (Finite.ftype ↥a).cardinality = k}

Equations

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

theorem Combinatorics.cardinality_subset_of_size {α : Type} [Finite α] {k : Nat} : (Finite.ftype ↥{s : Set α | (Finite.ftype ↥s).cardinality = k}).cardinality = (Finite.ftype α).cardinality.binom k

theorem Combinatorics.cardinality_strict_mono_of_size {α β : Type} [Finite α] [Finite β] [TotalOrder α] [TotalOrder β] : (Finite.ftype ↥{f : α → β | StrictMonotone f}).cardinality = (Finite.ftype β).cardinality.binom (Finite.ftype α).cardinality