parts_map — Mathlib

English

The parts of the image of a Finpartition under an order isomorphism e are exactly the map of the parts: (P.map e).parts = P.parts.map e.

Русский

Части отображения Finpartition под изоморфизмом порядка e равны отображению частей через e: (P.map e).parts = P.parts.map e.

LaTeX

$$$ (P.map\ u).parts = P.parts.map e$$$

Lean4

@[simp]
theorem parts_map {β : Type*} [Lattice β] [OrderBot β] {a : α} {e : α ≃o β} {P : Finpartition a} :
    (P.map e).parts = P.parts.map e :=
  rfl

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