Mathlib Map

Theorems · Definition · order theory

IsTrans.casesOn

{α : Sort u_1} →
  {r : α → α → Prop} →
    {motive : IsTrans α r → Sort u} →
      (t : IsTrans α r) → ((trans : ∀ (a b c : α), r a b → r b c → r a c) → motive ⋯) → motive t
Defined in
Mathlib.Order.Defs.Unbundled
Cited by
1 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZFSet.isOrdinal_iff_isTrans · cited by 3ZFSet.isOrdinal_iff_isTra…IsTrans · cited by 157IsTransIsTrans.casesOnCITED BYCITES

Cites1

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

  • IsTransstatement and proof · cited by 157

Cited by1

Results whose statement or proof uses this declaration.