Theorems · Definition · order theory
Heyting.Regular
(α : Type u_1) → [HeytingAlgebra α] → Type u_1
The Boolean algebra of Heyting regular elements.
- Defined in
- Mathlib.Order.Heyting.Regular
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- HeytingAlgebra
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.
- HeytingAlgebrastatement and proof · cited by 108
- Heyting.IsRegularproof · cited by 11
Cited by17
Results whose statement or proof uses this declaration.
- Heyting.Regular.valstatement · cited by 14
- Heyting.Regular.toRegularstatement · cited by 2
- Heyting.Regular.coe_injectivestatement · cited by 1
- Heyting.Regular.coe_botstatement · cited by 0
- Heyting.Regular.coe_complstatement and proof · cited by 0
- Heyting.Regular.coe_himpstatement and proof · cited by 0
- Heyting.Regular.coe_infstatement and proof · cited by 0
- Heyting.Regular.coe_injstatement and proof · cited by 0
- Heyting.Regular.coe_le_coestatement and proof · cited by 0
- Heyting.Regular.coe_lt_coestatement and proof · cited by 0
- Heyting.Regular.coe_sdiffstatement and proof · cited by 0
- Heyting.Regular.coe_supstatement and proof · cited by 0