Mathlib Map

Theorems · Theorem · order theory

mem_lowerClosure

∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {x : α}, x ∈ lowerClosure s ↔ ∃ a ∈ s, x ≤ a
Defined in
Mathlib.Order.UpperLower.Closure
Cited by
5 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

lowerClosure_singleton · cited by 8lowerClosure_singletonlowerClosure_image · cited by 3lowerClosure_imagecoe_lowerClosure · cited by 2coe_lowerClosureIsUpperSet.disjoint_lowerClosure_left · cited by 1IsUpperSet.disjoint_lower…LowerSet.iSup_Iic · cited by 0LowerSet.iSup_IicSet · cited by 53352SetPreorder · cited by 7952PreorderLowerSet · cited by 230LowerSetlowerClosure · cited by 83lowerClosuremem_lowerClosureCITED 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
  • LowerSetstatement · cited by 230
  • lowerClosurestatement · cited by 83

Cited by5

Results whose statement or proof uses this declaration.