Commit 2022-08-29 13:10 24b08ce6

View on Github →

feat(order/heyting/regular): Heyting-regular elements (#16033) Define Heyting-regular elements of an Heyting lattice, namely those a such that aᶜᶜ = a, and prove that they form a boolean algebra.

Estimated changes

Created src/order/heyting/regular.lean

added def boolean_algebra.of_regular

added theorem heyting.is_regular.himp

added theorem heyting.is_regular.inf

added def heyting.is_regular

added theorem heyting.is_regular_bot

added theorem heyting.is_regular_compl

added theorem heyting.is_regular_of_boolean

added theorem heyting.is_regular_of_decidable

added theorem heyting.is_regular_top

added theorem heyting.regular.coe_bot

added theorem heyting.regular.coe_compl

added theorem heyting.regular.coe_himp

added theorem heyting.regular.coe_inf

added theorem heyting.regular.coe_inj

added theorem heyting.regular.coe_injective

added theorem heyting.regular.coe_le_coe

added theorem heyting.regular.coe_lt_coe

added theorem heyting.regular.coe_sdiff

added theorem heyting.regular.coe_sup

added theorem heyting.regular.coe_to_regular

added theorem heyting.regular.coe_top

added def heyting.regular.gi

added def heyting.regular.to_regular

added theorem heyting.regular.to_regular_coe

added def heyting.regular