mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(order/heyting/regular): Heyting-regular elements

Open YaelDillies opened this issue 3 years ago • 1 comments

Define Heyting-regular elements of an Heyting lattice, namely those a such that aᶜᶜ = a, and prove that they form a boolean algebra.

  • [ ] depends on: #15305

Open in Gitpod

YaelDillies avatar Aug 12 '22 18:08 YaelDillies

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15305~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Aug 24 '22 21:08 mathlib-dependent-issues-bot

:v: 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.

bors[bot] avatar Aug 29 '22 12:08 bors[bot]

Or even,

bors r+

Vierkantor avatar Aug 29 '22 12:08 Vierkantor

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 29 '22 16:08 bors[bot]