Mathlib Map

Theorems · Definition · order theory

SupClosed

{α : Type u_3} → [SemilatticeSup α] → Set α → Prop

A set s is sup-closed if a ⊔ b ∈ s for all a ∈ s, b ∈ s.

Defined in
Mathlib.Order.SupClosed
Cited by
57 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
SemilatticeSup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

supClosure · cited by 33supClosureIsSublattice.supClosed · cited by 15IsSublattice.supClosedCompleteLattice.IsSupClosedCompact · cited by 9CompleteLattice.IsSupClos…supClosed_supClosure · cited by 8supClosed_supClosureBooleanSubalgebra.supClosed · cited by 7BooleanSubalgebra.supClos…SupClosed.finsetSup'_mem · cited by 5SupClosed.finsetSup'_memSupClosed.iSup_mem · cited by 5SupClosed.iSup_memSupClosed.sSup_mem · cited by 5SupClosed.sSup_memSublattice.supClosed · cited by 5Sublattice.supClosedCountableSupClosed.supClosed · cited by 3CountableSupClosed.supClo…SupClosed.biSup_mem · cited by 3SupClosed.biSup_memsupClosure_min · cited by 3supClosure_minLinearOrder.supClosed · cited by 2LinearOrder.supClosedFinset.univ_sups_univ · cited by 2Finset.univ_sups_univSupClosed.finsetSup_mem · cited by 2SupClosed.finsetSup_memSet · cited by 53352SetSemilatticeSup · cited by 785SemilatticeSupSupClosedCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • SemilatticeSupstatement and proof · cited by 785

Cited by67

Results whose statement or proof uses this declaration.