Zulip Chat Archive

Stream: maths

Topic: roption.dom vs multiplicity.finite


Johan Commelin (Dec 28 2020 at 11:59):

We have docs#multiplicity.finite and

lemma finite_iff_dom [decidable_rel (() : α  α  Prop)] {a b : α} :
  finite a b  (multiplicity a b).dom := iff.rfl

what do people think of defining enat.finite instead (as abbreviation for roption.dom)?
Because data.nat.enat has many occurences of x.dom for some x : enat, and I think x.finite looks much better.

Johan Commelin (Dec 28 2020 at 12:10):

Maybe enat.finite shouldn't replace multiplicity.finite... both defs could coexist.


Last updated: Dec 20 2023 at 11:08 UTC