theorem IsCompl.isComplemented {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} (h : IsCompl a b) : IsComplemented a

theorem IsCompl.isComplemented_left {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} (h : IsCompl a b) : IsComplemented a

Alias of IsCompl.isComplemented.

theorem IsCompl.isComplemented_right {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} (h : IsCompl a b) : IsComplemented b