[Merged by Bors] - feat(order/bounded_order): The lattice of complemented elements

[YaelDillies]

Define complementeds, the subtype of complemented elements, and show that it is a complemented bounded distributive lattice.

---

• depends on: [Merged by Bors] - chore(order/bounded_order): Rename is_complemented to complemented_lattice #16263

This is pretty tautological in itself. The motivation is when we get to Heyting algebras, as then complementeds is the right adjoint to the forgetful functor BoolAlg ⥤ HeytAlg.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(order/bounded_order): Rename is_complemented to complemented_lattice #16263
  By Dependent Issues (🤖). Happy coding!

[Vierkantor]

I'm still not quite convinced that the predicate + subtype approach is the best way to go. Although dot notation is convenient, won't it cause a lot of annoyance transporting between is_complemented and complementeds, as it is already for is_unit?

With this setup, we definitely need some explicit maps between complementeds and is_complemented, along the lines of what we have for units and is_unit.

[YaelDillies]

We now have quite a lot of experience with is_upper_set/upper_set, and it seems everything works smoothly. Of course there's some "morally duplicated" code, but IMO it's API making every use ever so less irritating.

I'm making complementeds into a reducible def for now because I'm not expecting to have a heavy enough use of it to justify duplicating subtype API.

[Vierkantor]

Thanks!

bors d+

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests