# mathlib3documentation

order.heyting.regular

# Heyting regular elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines Heyting regular elements, elements of an 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 #

• is_regular: a is Heyting-regular if aᶜᶜ = a.
• regular: The subtype of Heyting-regular elements.
• regular.boolean_algebra: Heyting-regular elements form a boolean algebra.

## References #

def heyting.is_regular {α : Type u_1} [has_compl α] (a : α) :
Prop

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

Equations
Instances for heyting.is_regular
@[protected]
theorem heyting.is_regular.eq {α : Type u_1} [has_compl α] {a : α} :
@[protected, instance]
Equations
theorem heyting.is_regular_bot {α : Type u_1}  :
theorem heyting.is_regular_top {α : Type u_1}  :
theorem heyting.is_regular.inf {α : Type u_1} {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :
theorem heyting.is_regular.himp {α : Type u_1} {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :
theorem heyting.is_regular_compl {α : Type u_1} (a : α) :
@[protected]
theorem heyting.is_regular.disjoint_compl_left_iff {α : Type u_1} {a b : α} (ha : heyting.is_regular a) :
b b a
@[protected]
theorem heyting.is_regular.disjoint_compl_right_iff {α : Type u_1} {a b : α} (hb : heyting.is_regular b) :
b a b
@[reducible]
def boolean_algebra.of_regular {α : Type u_1} (h : (a : α), heyting.is_regular (a a)) :

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

Equations
def heyting.regular (α : Type u_1)  :
Type u_1

The boolean algebra of Heyting regular elements.

Equations
• = {a //
Instances for heyting.regular
@[protected, instance]
def heyting.regular.has_coe {α : Type u_1}  :
α
Equations
theorem heyting.regular.coe_injective {α : Type u_1}  :
@[simp]
theorem heyting.regular.coe_inj {α : Type u_1} {a b : heyting.regular α} :
a = b a = b
@[protected, instance]
def heyting.regular.has_top {α : Type u_1}  :
Equations
@[protected, instance]
def heyting.regular.has_bot {α : Type u_1}  :
Equations
@[protected, instance]
def heyting.regular.has_inf {α : Type u_1}  :
Equations
@[protected, instance]
def heyting.regular.has_himp {α : Type u_1}  :
Equations
@[protected, instance]
def heyting.regular.has_compl {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem heyting.regular.coe_top {α : Type u_1}  :
@[simp, norm_cast]
theorem heyting.regular.coe_bot {α : Type u_1}  :
@[simp, norm_cast]
theorem heyting.regular.coe_inf {α : Type u_1} (a b : heyting.regular α) :
(a b) = a b
@[simp, norm_cast]
theorem heyting.regular.coe_himp {α : Type u_1} (a b : heyting.regular α) :
(a b) = a b
@[simp, norm_cast]
theorem heyting.regular.coe_compl {α : Type u_1} (a : heyting.regular α) :
@[protected, instance]
def heyting.regular.inhabited {α : Type u_1}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def heyting.regular.bounded_order {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem heyting.regular.coe_le_coe {α : Type u_1} {a b : heyting.regular α} :
a b a b
@[simp, norm_cast]
theorem heyting.regular.coe_lt_coe {α : Type u_1} {a b : heyting.regular α} :
a < b a < b
def heyting.regular.to_regular {α : Type u_1}  :

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

Equations
@[simp, norm_cast]
theorem heyting.regular.coe_to_regular {α : Type u_1} (a : α) :
@[simp]
theorem heyting.regular.to_regular_coe {α : Type u_1} (a : heyting.regular α) :

The Galois insertion between regular.to_regular and coe.

Equations
@[protected, instance]
def heyting.regular.lattice {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem heyting.regular.coe_sup {α : Type u_1} (a b : heyting.regular α) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem heyting.regular.coe_sdiff {α : Type u_1} (a b : heyting.regular α) :
(a \ b) = a (b)
theorem heyting.is_regular_of_boolean {α : Type u_1} (a : α) :
@[nolint]
theorem heyting.is_regular_of_decidable (p : Prop) [decidable p] :

A decidable proposition is intuitionistically Heyting-regular.