embSigma — Mathlib

English

The default equals the atomic partition (reaffirmed).

Русский

Повторное утверждение: значение по умолчанию равно атомарному разбиению.

LaTeX

$$$\text{default} = \text{atomic } n$$$

Lean4

/-- Embedding of ordered finpartitions in a sigma type. The sigma type on the right is quite big,
but this is enough to get finiteness of ordered finpartitions. -/
def embSigma (n : ℕ) :
    OrderedFinpartition n → (Σ (l : Fin (n + 1)), Σ (p : Fin l → Fin (n + 1)), Π (i : Fin l), (Fin (p i) → Fin n)) :=
  fun c ↦
  ⟨⟨c.length, Order.lt_add_one_iff.mpr c.length_le⟩, fun m ↦ ⟨c.partSize m, Order.lt_add_one_iff.mpr (c.partSize_le m)⟩,
    fun j ↦ c.emb j⟩

Похожие утверждения