Mathlib Map

Theorems · Theorem · order theory

isGLB_congr

∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a : α}, lowerBounds s = lowerBounds t → (IsGLB s a ↔ IsGLB t a)
Defined in
Mathlib.Order.Bounds.Basic
Cited by
2 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isGLB_iUnion_iff_of_isGLB · cited by 0isGLB_iUnion_iff_of_isGLBisGLB_iUnion_iff_of_isLUB · cited by 0isGLB_iUnion_iff_of_isLUBSet · cited by 53352SetPreorder · cited by 7952PreorderIsGLB · cited by 213IsGLBlowerBounds · cited by 212lowerBoundsIsGreatest · cited by 112IsGreatestisGLB_congrCITED BYCITES

Cites5

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
  • IsGLBstatement and proof · cited by 213
  • lowerBoundsstatement and proof · cited by 212
  • IsGreatestproof · cited by 112

Cited by2

Results whose statement or proof uses this declaration.