[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
⊢ IsRegular ⊥
[PROOFSTEP]
rw [IsRegular, compl_bot, compl_top]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
⊢ IsRegular ⊤
[PROOFSTEP]
rw [IsRegular, compl_top, compl_bot]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⊓ b)
[PROOFSTEP]
rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⇨ b)
[PROOFSTEP]
rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
⊢ Disjoint aᶜ b ↔ b ≤ a
[PROOFSTEP]
rw [← le_compl_iff_disjoint_left, ha.eq]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ Disjoint a bᶜ ↔ a ≤ b
[PROOFSTEP]
rw [← le_compl_iff_disjoint_right, hb.eq]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ a ⊔ aᶜ = ⊤
[PROOFSTEP]
erw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b c : Regular α
⊢ ↑((a ⊔ b) ⊓ (a ⊔ c)) ≤ ↑(a ⊔ b ⊓ c)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b c : Regular α
⊢ (↑a ⊔ ↑b)ᶜᶜ ⊓ (↑a ⊔ ↑c)ᶜᶜ ≤ (↑a ⊔ ↑b ⊓ ↑c)ᶜᶜ
[PROOFSTEP]
rw [sup_inf_left, compl_compl_inf_distrib]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a : Regular α
⊢ ↑⊤ ≤ ↑(a ⊔ aᶜ)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a : Regular α
⊢ ⊤ ≤ (↑a ⊔ (↑a)ᶜ)ᶜᶜ
[PROOFSTEP]
rw [compl_sup, inf_compl_eq_bot, compl_bot]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b : Regular α
⊢ ↑(a ⇨ b) = ↑(b ⊔ aᶜ)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b : Regular α
⊢ ↑a ⇨ ↑b = (↑b ⊔ (↑a)ᶜ)ᶜᶜ
[PROOFSTEP]
rw [compl_sup, a.prop.eq]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b : Regular α
⊢ ↑a ⇨ ↑b = ((↑b)ᶜ ⊓ ↑a)ᶜ
[PROOFSTEP]
refine' eq_of_forall_le_iff fun c => le_himp_iff.trans _
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b : Regular α
c : α
⊢ c ⊓ ↑a ≤ ↑b ↔ c ≤ ((↑b)ᶜ ⊓ ↑a)ᶜ
[PROOFSTEP]
rw [le_compl_iff_disjoint_right, disjoint_left_comm]
[GOAL]
α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
src✝³ : Lattice (Regular α) := lattice
src✝² : BoundedOrder (Regular α) := boundedOrder
src✝¹ : HImp (Regular α) := himp
src✝ : HasCompl (Regular α) := hasCompl
a b : Regular α
c : α
⊢ c ⊓ ↑a ≤ ↑b ↔ Disjoint (↑b)ᶜ (c ⊓ ↑a)
[PROOFSTEP]
rw [b.prop.disjoint_compl_left_iff]
