Mathlib Map

Theorems · Definition · category theory

BddLat.casesOn

{motive : BddLat → Sort u} →
  (t : BddLat) →
    ((toLat : Lat) →
        [isBoundedOrder : BoundedOrder ↑toLat] → motive { toLat := toLat, isBoundedOrder := isBoundedOrder }) →
      motive t
Defined in
Mathlib.Order.Category.BddLat
Cited by
0 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BddLat.noConfusion · cited by 0BddLat.noConfusionBddLat.noConfusionType · cited by 0BddLat.noConfusionTypeBoundedOrder · cited by 270BoundedOrderLat.carrier · cited by 58Lat.carrierLat · cited by 43LatBddLat · cited by 27BddLatBddLat.casesOnCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • BoundedOrderstatement and proof · cited by 270
  • Lat.carrierstatement and proof · cited by 58
  • Latstatement and proof · cited by 43
  • BddLatstatement and proof · cited by 27

Cited by2

Results whose statement or proof uses this declaration.