Mathlib Map

Theorems · Theorem · logic and foundations

Trunc.ind

∀ {α : Sort u_1} {β : Trunc α → Prop}, (∀ (a : α), β (Trunc.mk a)) → ∀ (q : Trunc α), β q
Defined in
Mathlib.Data.Quot
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Trunc.induction_on · cited by 5Trunc.induction_onFinset.mem_piAntidiag · cited by 1Finset.mem_piAntidiagTrunc · cited by 39TruncTrunc.mk · cited by 21Trunc.mkTrunc.indCITED BYCITES

Cites2

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

  • Truncstatement and proof · cited by 39
  • Trunc.mkstatement · cited by 21

Cited by2

Results whose statement or proof uses this declaration.