# Heyting regular elements #

This file defines Heyting regular elements, elements of a Heyting algebra that are their own double complement, and proves that they form a boolean algebra.

From a logic standpoint, this means that we can perform classical logic within intuitionistic logic by simply double-negating all propositions. This is practical for synthetic computability theory.

## Main declarations #

• IsRegular: a is Heyting-regular if aᶜᶜ = a.
• Regular: The subtype of Heyting-regular elements.
• Regular.BooleanAlgebra: Heyting-regular elements form a boolean algebra.

## References #

def Heyting.IsRegular {α : Type u_1} [] (a : α) :

An element of a Heyting algebra is regular if its double complement is itself.

Equations
Instances For
theorem Heyting.IsRegular.eq {α : Type u_1} [] {a : α} :
a = a
instance Heyting.IsRegular.decidablePred {α : Type u_1} [] [] :
DecidablePred Heyting.IsRegular
Equations
theorem Heyting.isRegular_bot {α : Type u_1} [] :
theorem Heyting.isRegular_top {α : Type u_1} [] :
theorem Heyting.IsRegular.inf {α : Type u_1} [] {a : α} {b : α} (ha : ) (hb : ) :
theorem Heyting.IsRegular.himp {α : Type u_1} [] {a : α} {b : α} (ha : ) (hb : ) :
theorem Heyting.isRegular_compl {α : Type u_1} [] (a : α) :
theorem Heyting.IsRegular.disjoint_compl_left_iff {α : Type u_1} [] {a : α} {b : α} (ha : ) :
b a
theorem Heyting.IsRegular.disjoint_compl_right_iff {α : Type u_1} [] {a : α} {b : α} (hb : ) :
a b
@[reducible, inline]
abbrev BooleanAlgebra.ofRegular {α : Type u_1} [] (h : ∀ (a : α), Heyting.IsRegular (a a)) :

A Heyting algebra with regular excluded middle is a boolean algebra.

Equations
• = let_fun this := ; let __src := inst; let __src_1 := GeneralizedHeytingAlgebra.toDistribLattice; BooleanAlgebra.mk
Instances For
def Heyting.Regular (α : Type u_1) [] :
Type u_1

The boolean algebra of Heyting regular elements.

Equations
• = { a : α // }
Instances For
def Heyting.Regular.val {α : Type u_1} [] :
α

The coercion Regular α → α

Equations
• Heyting.Regular.val = Subtype.val
Instances For
theorem Heyting.Regular.prop {α : Type u_1} [] (a : ) :
instance Heyting.Regular.instCoeOut {α : Type u_1} [] :
Equations
• Heyting.Regular.instCoeOut = { coe := Heyting.Regular.val }
theorem Heyting.Regular.coe_injective {α : Type u_1} [] :
Function.Injective Heyting.Regular.val
@[simp]
theorem Heyting.Regular.coe_inj {α : Type u_1} [] {a : } {b : } :
a = b a = b
instance Heyting.Regular.top {α : Type u_1} [] :
Equations
• Heyting.Regular.top = { top := , }
instance Heyting.Regular.bot {α : Type u_1} [] :
Equations
• Heyting.Regular.bot = { bot := , }
instance Heyting.Regular.inf {α : Type u_1} [] :
Equations
• Heyting.Regular.inf = { inf := fun (a b : ) => a b, }
instance Heyting.Regular.himp {α : Type u_1} [] :
Equations
• Heyting.Regular.himp = { himp := fun (a b : ) => a b, }
instance Heyting.Regular.hasCompl {α : Type u_1} [] :
Equations
• Heyting.Regular.hasCompl = { compl := fun (a : ) => (a), }
@[simp]
theorem Heyting.Regular.coe_top {α : Type u_1} [] :
=
@[simp]
theorem Heyting.Regular.coe_bot {α : Type u_1} [] :
=
@[simp]
theorem Heyting.Regular.coe_inf {α : Type u_1} [] (a : ) (b : ) :
(a b) = a b
@[simp]
theorem Heyting.Regular.coe_himp {α : Type u_1} [] (a : ) (b : ) :
(a b) = a b
@[simp]
theorem Heyting.Regular.coe_compl {α : Type u_1} [] (a : ) :
a = (a)
instance Heyting.Regular.instInhabited {α : Type u_1} [] :
Equations
• Heyting.Regular.instInhabited = { default := }
instance Heyting.Regular.instSemilatticeInf {α : Type u_1} [] :
Equations
instance Heyting.Regular.boundedOrder {α : Type u_1} [] :
Equations
@[simp]
theorem Heyting.Regular.coe_le_coe {α : Type u_1} [] {a : } {b : } :
a b a b
@[simp]
theorem Heyting.Regular.coe_lt_coe {α : Type u_1} [] {a : } {b : } :
a < b a < b
def Heyting.Regular.toRegular {α : Type u_1} [] :

Regularization of a. The smallest regular element greater than a.

Equations
• Heyting.Regular.toRegular = { toFun := fun (a : α) => a, , monotone' := }
Instances For
@[simp]
theorem Heyting.Regular.coe_toRegular {α : Type u_1} [] (a : α) :
(Heyting.Regular.toRegular a) = a
@[simp]
theorem Heyting.Regular.toRegular_coe {α : Type u_1} [] (a : ) :
Heyting.Regular.toRegular a = a
def Heyting.Regular.gi {α : Type u_1} [] :
GaloisInsertion (Heyting.Regular.toRegular) Heyting.Regular.val

The Galois insertion between Regular.toRegular and coe.

Equations
• Heyting.Regular.gi = { choice := fun (a : α) (ha : (Heyting.Regular.toRegular a) a) => a, , gc := , le_l_u := , choice_eq := }
Instances For
instance Heyting.Regular.lattice {α : Type u_1} [] :
Equations
• Heyting.Regular.lattice = Heyting.Regular.gi.liftLattice
@[simp]
theorem Heyting.Regular.coe_sup {α : Type u_1} [] (a : ) (b : ) :
(a b) = (a b)
instance Heyting.Regular.instBooleanAlgebra {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Heyting.Regular.coe_sdiff {α : Type u_1} [] (a : ) (b : ) :
(a \ b) = a (b)
theorem Heyting.isRegular_of_boolean {α : Type u_1} [] (a : α) :

A decidable proposition is intuitionistically Heyting-regular.