# Co-Heyting boundary #

The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation with itself. The boundary in the co-Heyting algebra of closed sets coincides with the topological boundary.

## Main declarations #

`Coheyting.boundary`

: Co-Heyting boundary.`Coheyting.boundary a = a ⊓ ￢a`

## Notation #

`∂ a`

is notation for `Coheyting.boundary a`

in locale `Heyting`

.

The boundary of an element of a co-Heyting algebra is the intersection of its Heyting negation
with itself. Note that this is always `⊥`

for a boolean algebra.

## Equations

- Coheyting.boundary a = a ⊓ ￢a

## Instances For

The boundary of an element of a co-Heyting algebra.

## Equations

- Heyting.«term∂_» = Lean.ParserDescr.node `Heyting.term∂_ 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∂ ") (Lean.ParserDescr.cat `term 120))

## Instances For

theorem
Coheyting.inf_hnot_self
{α : Type u_1}
[CoheytingAlgebra α]
(a : α)
:

a ⊓ ￢a = Coheyting.boundary a

theorem
Coheyting.boundary_le_hnot
{α : Type u_1}
[CoheytingAlgebra α]
{a : α}
:

Coheyting.boundary a ≤ ￢a

@[simp]

@[simp]

@[simp]

theorem
Coheyting.boundary_hnot_hnot
{α : Type u_1}
[CoheytingAlgebra α]
(a : α)
:

Coheyting.boundary (￢￢a) = Coheyting.boundary (￢a)

@[simp]

theorem
Coheyting.boundary_inf
{α : Type u_1}
[CoheytingAlgebra α]
(a : α)
(b : α)
:

Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊓ b ⊔ a ⊓ Coheyting.boundary b

**Leibniz rule** for the co-Heyting boundary.

theorem
Coheyting.boundary_inf_le
{α : Type u_1}
[CoheytingAlgebra α]
{a : α}
{b : α}
:

Coheyting.boundary (a ⊓ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b

theorem
Coheyting.boundary_sup_le
{α : Type u_1}
[CoheytingAlgebra α]
{a : α}
{b : α}
:

Coheyting.boundary (a ⊔ b) ≤ Coheyting.boundary a ⊔ Coheyting.boundary b

theorem
Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left
{α : Type u_1}
[CoheytingAlgebra α]
{a : α}
{b : α}
:

Coheyting.boundary a ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)

theorem
Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right
{α : Type u_1}
[CoheytingAlgebra α]
{a : α}
{b : α}
:

Coheyting.boundary b ≤ Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b)

theorem
Coheyting.boundary_sup_sup_boundary_inf
{α : Type u_1}
[CoheytingAlgebra α]
(a : α)
(b : α)
:

Coheyting.boundary (a ⊔ b) ⊔ Coheyting.boundary (a ⊓ b) = Coheyting.boundary a ⊔ Coheyting.boundary b

@[simp]

theorem
Coheyting.hnot_hnot_sup_boundary
{α : Type u_1}
[CoheytingAlgebra α]
(a : α)
:

￢￢a ⊔ Coheyting.boundary a = a

@[simp]