Theorems · Theorem · order theory
sup_idem
∀ {α : Type u} [inst : SemilatticeSup α] (a : α), a ⊔ a = a- Defined in
- Mathlib.Order.Lattice
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext
- Assumes
- SemilatticeSup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SemilatticeSupstatement and proof · cited by 785
- sup_of_le_leftproof · cited by 218
Cited by29
Results whose statement or proof uses this declaration.
- sdiff_idemproof · cited by 12
- posPart_zeroproof · cited by 12
- Finset.union_idempotentproof · cited by 11
- symmDiff_selfproof · cited by 8
- sup_sup_distrib_rightproof · cited by 6
- Function.support_supproof · cited by 4
- sup_div_inf_eq_mabs_divproof · cited by 3
- UV.compress_idemproof · cited by 3
- sup_sub_inf_eq_abs_subproof · cited by 3
- Function.mulSupport_supproof · cited by 3
- Filter.Tendsto.max_rightproof · cited by 2
- Metric.hausdorffEDist_selfproof · cited by 2