Mathlib Map

Theorems · Definition · order theory

lowerClosure

{α : Type u_1} → [inst : Preorder α] → Set α → LowerSet α

The least lower set containing a given set.

Defined in
Mathlib.Order.UpperLower.Closure
Cited by
83 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.truncatedSup · cited by 19Finset.truncatedSupsubset_lowerClosure · cited by 12subset_lowerClosurelowerClosure_singleton · cited by 8lowerClosure_singletonUpperSet.sdiff · cited by 8UpperSet.sdifflowerClosure_min · cited by 6lowerClosure_minSet.OrdConnected.upperClosure_inter_lowerClosure · cited by 5OrdConnected.upperClosure…mem_lowerClosure · cited by 5mem_lowerClosureFinset.truncatedSup_of_mem · cited by 4Finset.truncatedSup_of_memFinset.truncatedSup_of_notMem · cited by 4Finset.truncatedSup_of_no…Topology.IsUpperSet.closure_eq_lowerClosure · cited by 3IsUpperSet.closure_eq_low…lowerClosure_iUnion · cited by 3lowerClosure_iUnionlowerClosure_image · cited by 3lowerClosure_imagelowerClosure_le · cited by 3lowerClosure_lebddAbove_lowerClosure · cited by 3bddAbove_lowerClosuregc_lowerClosure_coe · cited by 3gc_lowerClosure_coeSet · cited by 53352SetPreorder · cited by 7952PreorderSet.ofPred · cited by 6101Set.ofPredLowerSet · cited by 230LowerSetlowerClosureCITED BYCITES

Cites4

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
  • Preorderstatement and proof · cited by 7,952
  • Set.ofPredproof · cited by 6,101
  • LowerSetstatement · cited by 230

Cited by89

Results whose statement or proof uses this declaration.