lower sets (#13069)

Commit

3 years ago

feat(order/upper_lower): Principal upper/lower sets (#13069) Define `upper_set.Ici` and `lower_set.Iic`. Also add membership lemmas for the lattice operations.

Author

YaelDillies

Parents

d790b4b8

mathlib 546618eb - feat(order/upper_lower): Principal upper/lower sets (#13069)

mathlib
546618eb - feat(order/upper_lower): Principal upper/lower sets (#13069)