partscopyEquiv — Mathlib

English

There is a natural equivalence between the subtype of parts and the subtype of parts of a copy (duplicated entry).

Русский

Существует естественная эквивалентность между подтипом частей и подтипом частей копии.

LaTeX

$$$(P.copy hst)\;\cong\; P$$$

Lean4

/-- The natural equivalence between the subtype of parts and the subtype of parts of a copy. -/
@[simps!]
def partscopyEquiv {t : α} (P : Partition s) (hst : s = t) : ↥(P.copy hst) ≃ ↥P :=
  Equiv.setCongr rfl

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