Theorems · Definition
Compl.compl
{α : Type u_1} → [self : Compl α] → α → αSet / lattice complement
Conventions for notations in identifiers:
* The recommended spelling of ᶜ in identifiers is compl.
- Defined in
- Mathlib.Order.Notation
- Cited by
- 2,925 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Compl
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complstatement and proof · cited by 11
Cited by3,139
Results whose statement or proof uses this declaration.
- spectrumproof · cited by 510
- Ideal.primeComplproof · cited by 462
- Bornology.IsBoundedproof · cited by 293
- compl_complstatement · cited by 229
- MeasurableSet.complstatement · cited by 172
- Filter.cocompactproof · cited by 141
- IsClosed.isOpen_complstatement · cited by 126
- SSet.nonDegenerateproof · cited by 106
- IsAntichainproof · cited by 105
- MeasureTheory.Measure.MutuallySingularproof · cited by 91
- AccPtproof · cited by 75
- Filter.comap_comapproof · cited by 69
Showing the 200 most cited of 3,139.