constructor
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ a ≤ bᶜ ⊔ c
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c → a ≤ bᶜ ⊔ c

case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜ ⊔ c → a ⊓ b ≤ c