Mathlib Map

Theorems · Definition · order theory

InfClosed

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

A set s is inf-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
SemilatticeInf
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

infClosure · cited by 21infClosureIsSublattice.infClosed · cited by 15IsSublattice.infClosedBooleanSubalgebra.infClosed · cited by 7BooleanSubalgebra.infClos…Sublattice.infClosed · cited by 5Sublattice.infClosedinfClosed_infClosure · cited by 5infClosed_infClosureInfClosed.finsetInf'_mem · cited by 5InfClosed.finsetInf'_meminfClosure_eq_self · cited by 4infClosure_eq_selfInfClosed.iInf_mem · cited by 4InfClosed.iInf_memInfClosed.sInf_mem · cited by 4InfClosed.sInf_meminfClosed_univ · cited by 3infClosed_univinfClosure_min · cited by 3infClosure_minInfClosed.iInf_mem_of_nonempty · cited by 3InfClosed.iInf_mem_of_non…CountableInfClosed.infClosed · cited by 3CountableInfClosed.infClo…Finset.univ_infs_univ · cited by 2Finset.univ_infs_univSublattice.infClosed' · cited by 2Sublattice.infClosed'Set · cited by 53352SetSemilatticeInf · cited by 634SemilatticeInfInfClosedCITED 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
  • SemilatticeInfstatement and proof · cited by 634

Cited by66

Results whose statement or proof uses this declaration.