mathlib3
5709b0d8 - feat(order/complete_lattice): missing API lemmas about the prod instance (#18029)

Commit

2 years ago

feat(order/complete_lattice): missing API lemmas about the prod instance (#18029) This adds lemmas about how `fst`, `snd`, and `swap` interact with `Sup` and `Inf`.

Author

eric-wieser

Parents

40acfb6a

mathlib3 5709b0d8 - feat(order/complete_lattice): missing API lemmas about the prod instance (#18029)

mathlib3
5709b0d8 - feat(order/complete_lattice): missing API lemmas about the prod instance (#18029)