copy — Mathlib

English

There is a way to regard a Finpartition a as a Finpartition b when a = b; this is a type-preserving reidentification of the partition.

Русский

Существует способ рассмотреть Finpartition a как Finpartition b при условии a = b; это сохранение типа для разбиения.

LaTeX

$$$\\forall a,b\\, (P : \\mathrm{Finpartition} a), (Eq\\ a\\ b) \\Rightarrow (P.copy\\ h) : \\mathrm{Finpartition} b$$$

Lean4

/-- Changes the type of a finpartition to an equal one. -/
@[simps]
def copy {a b : α} (P : Finpartition a) (h : a = b) : Finpartition b
    where
  parts := P.parts
  supIndep := P.supIndep
  sup_parts := h ▸ P.sup_parts
  bot_notMem := P.bot_notMem

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