Zulip Chat Archive
Stream: mathlib4
Topic: lift_pair etc
Yury G. Kudryashov (Jan 21 2023 at 21:11):
One of the few remaining errors in order.filter.basic is about docs#lift_pair
Yury G. Kudryashov (Jan 21 2023 at 21:12):
It seems that we don't have this instance in Lean 4. Should we add it? Or should we avoid it?
Yury G. Kudryashov (Jan 23 2023 at 08:22):
I removed the lemma in order.filter.basic that depended on this instance.
Last updated: Dec 20 2023 at 11:08 UTC