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: May 02 2025 at 03:31 UTC