complement in CompleteLattice

Stream: mathlib4

[Pieter Cuijpers]

Bit of a beginner question, perhaps.

For a complete lattice, it makes sense to me to define a complement as

instance [CompleteLattice α] : HasCompl α := {compl := λ x => supₛ { z | x ⊓ z ≤ ⊥ }}

I thought this would actually already have been formalized in Mathlib, but can't find it.

• Am I overlooking an existing definition somewhere here?
• Should I consider Heyting algebra's instead? I know they do have a complement.
• The "HasCompl" class does not require me to prove that the operator actually is a complement. Why is that?

[Kevin Buzzard]

The last one I can answer: HasCompl is simply a "notation typeclass", that is, it's just a way of registering the ᶜ notation on a type. It doesn't have any mathematical content.

[Yaël Dillies]

The answer is that this is currently a gap in mathlib which will be closed up by #10560

[Pieter Cuijpers]

Thanks, that clears it up quite a bit for me :-)