Theorems · Definition · order theory
latticeClosure
{α : Type u_3} → [Lattice α] → ClosureOperator (Set α)Every set in a join-semilattice generates a set closed under join.
- Defined in
- Mathlib.Order.SupClosed
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Lattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Latticestatement and proof · cited by 916
- ClosureOperatorstatement · cited by 371
- IsSublatticeproof · cited by 28
- ClosureOperator.ofCompletePredproof · cited by 4
- isSublattice_sInterproof · cited by 1
Cited by24
Results whose statement or proof uses this declaration.
- subset_latticeClosurestatement and proof · cited by 6
- isSublattice_latticeClosurestatement and proof · cited by 5
- latticeClosure_minstatement · cited by 4
- four_functions_theoremproof · cited by 3
- supClosure_infClosurestatement · cited by 2
- latticeClosure_eq_selfstatement and proof · cited by 1
- latticeClosure_sup_inf_inductionstatement and proof · cited by 1
- Set.Finite.latticeClosurestatement · cited by 1
- BooleanSubalgebra.latticeClosure_subset_closurestatement · cited by 1
- image_latticeClosurestatement and proof · cited by 1
- image_latticeClosure'statement and proof · cited by 1
- compl_image_latticeClosurestatement · cited by 1