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