Theorems · Definition · order theory
Coheyting.boundary
{α : Type u_1} → [CoheytingAlgebra α] → α → α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.
- Defined in
- Mathlib.Order.Heyting.Boundary
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- CoheytingAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CoheytingAlgebrastatement and proof · cited by 96
- HNot.hnotproof · cited by 83
Cited by24
Results whose statement or proof uses this declaration.
- Coheyting.hnot_boundarystatement · cited by 3
- Coheyting.boundary_boundarystatement and proof · cited by 2
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_leftstatement · cited by 2
- Coheyting.boundary_sup_lestatement and proof · cited by 2
- Coheyting.hnot_hnot_sup_boundarystatement · cited by 2
- boundary_principalstatement · cited by 1
- le_cofinite_iff_boundarystatement · cited by 1
- Coheyting.boundary_infstatement · cited by 1
- Coheyting.boundary_inf_lestatement · cited by 1
- Coheyting.boundary_lestatement · cited by 1
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_rightstatement and proof · cited by 1
- Coheyting.inf_hnot_selfstatement · cited by 1