mathlib3 documentation

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 #

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.inf {α : Type u_1} [heyting_algebra α] {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :
theorem heyting.is_regular.himp {α : Type u_1} [heyting_algebra α] {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :
@[protected]
@[protected]
@[reducible]

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

Equations
@[protected, instance]
Equations
@[simp]
theorem heyting.regular.coe_inj {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :
a = b a = b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem heyting.regular.coe_inf {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :
(a b) = a b
@[simp, norm_cast]
theorem heyting.regular.coe_himp {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :
(a b) = a b
@[simp, norm_cast]
theorem heyting.regular.coe_compl {α : Type u_1} [heyting_algebra α] (a : heyting.regular α) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem heyting.regular.coe_le_coe {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :
a b a b
@[simp, norm_cast]
theorem heyting.regular.coe_lt_coe {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :
a < b a < b

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

Equations
@[simp, norm_cast]

The Galois insertion between regular.to_regular and coe.

Equations
@[simp, norm_cast]
theorem heyting.regular.coe_sup {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :
@[simp, norm_cast]
theorem heyting.regular.coe_sdiff {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :
(a \ b) = a (b)
@[nolint]

A decidable proposition is intuitionistically Heyting-regular.