{α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      {β : Type u_2} →
        [inst_2 : Lattice β] → [inst_3 : OrderBot β] → {a : α} → (e : α ≃o β) → Finpartition a → Finpartition (e a)