Commit 2023-01-01 18:42 25a13655

View on Github →

feat port: Order.Heyting.Regular (#1269) Only non-trivial things here were introducing val and prop

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Heyting/Regular.lean

added def BooleanAlgebra.ofRegular

added theorem Heyting.IsRegular.himp

added theorem Heyting.IsRegular.inf

added def Heyting.IsRegular

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 theorem Heyting.Regular.prop

added def Heyting.Regular.toRegular

added theorem Heyting.Regular.to_regular_coe

added def Heyting.Regular.val

added def Heyting.Regular

added theorem Heyting.isRegular_bot

added theorem Heyting.isRegular_compl

added theorem Heyting.isRegular_top

added theorem Heyting.is_regular_of_boolean

added theorem Heyting.is_regular_of_decidable