English
A Heyting algebra in which every a ∨ aᶜ is regular is a Boolean algebra.
Русский
Алгебра Хейтинга, в которой каждый элемент a ∨ aᶜ является регулярным, является буловой алгеброй.
LaTeX
$$$\\left(\\forall a:\\\\alpha, \\mathrm{IsRegular}(a \\lor a^c)\\right) \\Rightarrow \\mathrm{BooleanAlgebra}(\\alpha)$$$
Lean4
/-- A Heyting algebra with regular excluded middle is a Boolean algebra. -/
abbrev _root_.BooleanAlgebra.ofRegular (h : ∀ a : α, IsRegular (a ⊔ aᶜ)) : BooleanAlgebra α :=
have : ∀ a : α, IsCompl a aᶜ := fun a =>
⟨disjoint_compl_right, codisjoint_iff.2 <| by rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]⟩
{ ‹HeytingAlgebra α›,
GeneralizedHeytingAlgebra.toDistribLattice with
himp_eq := fun _ _ => eq_of_forall_le_iff fun _ => le_himp_iff.trans (this _).le_sup_right_iff_inf_left_le.symm
inf_compl_le_bot := fun _ => (this _).1.le_bot
top_le_sup_compl := fun _ => (this _).2.top_le }
