English
Transferring a Finpartition along an order isomorphism e: α ≃o β yields a Finpartition on e a by mapping the parts via e.
Русский
Перенос разбиения Finpartition через тождество порядка e: α ≃o β даёт Finpartition на e a путём отображения частей через e.
LaTeX
$$$ \\mathrm{Finpartition.map}\\ e\\ P : \\mathrm{Finpartition}(e a) $$$
Lean4
/-- Transfer a finpartition over an order isomorphism. -/
def map {β : Type*} [Lattice β] [OrderBot β] {a : α} (e : α ≃o β) (P : Finpartition a) : Finpartition (e a)
where
parts := P.parts.map e
supIndep u hu _ hb hbu _ hx
hxu := by
rw [← map_symm_subset] at hu
simp only [mem_map_equiv] at hb
have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
· rw [← e.symm.map_bot] at this
exact e.symm.map_rel_iff.mp this
· convert e.symm.map_rel_iff.mpr hxu
rw [map_finset_sup, sup_map]
rfl
sup_parts := by simp [← P.sup_parts]
bot_notMem := by
rw [mem_map_equiv]
convert P.bot_notMem
exact e.symm.map_bot
