Theorems · Theorem · order theory

GeneralizedBooleanAlgebra.inf_inf_sdiff

∀ {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α), a ⊓ b ⊓ a \ b = ⊥

For any a, b, (a ⊓ b) ⊓ (a / b) = ⊥

Defined in

Mathlib.Order.BooleanAlgebra.Defs

Cited by

1 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GeneralizedBooleanAlgebra