Subset relation for Finmap

Stream: Is there code for X?

[Ka Wing Li]

Is there any relation like $M_1 \subseteq M_2$ for finite map $M$?

[Kenny Lau]

@Ka Wing Li there are only 117 declarations about Finmap, and i'm afraid none of them is about an ordering - but you can define one easily!

[Kenny Lau]

import Mathlib.Data.Finmap

namespace Finmap

variable {α : Type*} {i : α → Type*}

instance : PartialOrder (Finmap i) :=
  PartialOrder.lift entries fun _ _ ↦ ext

lemma le_def (x y : Finmap i) : x ≤ y ↔ x.entries ⊆ y.entries :=
  Multiset.le_iff_subset x.nodup_entries

end Finmap

[Ka Wing Li]

Thanks! I get the idea of how to define relations.