Mathlib Map

Theorems · Definition · logic and foundations

Fact.casesOn

{p : Prop} → {motive : Fact p → Sort u} → (t : Fact p) → ((out : p) → motive ⋯) → motive t
Defined in
Mathlib.Logic.Basic
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.

ExpChar.exists · cited by 11ExpChar.existsFact · cited by 2726FactFact.casesOnCITED BYCITES

Cites1

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

  • Factstatement and proof · cited by 2,726

Cited by1

Results whose statement or proof uses this declaration.