Mathlib Map

Theorems · Definition · logic and foundations

Trunc.bind

{α : Sort u_1} → {β : Sort u_2} → Trunc α → (α → Trunc β) → Trunc β

The bind operator for the Trunc monad.

Defined in
Mathlib.Data.Quot
Cited by
0 results in Mathlib
Foundations
Depth 12 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DFinsupp.zipWith · cited by 7DFinsupp.zipWithDFinsupp.rangeIcc · cited by 5DFinsupp.rangeIccDFinsupp.sigmaUncurry · cited by 5DFinsupp.sigmaUncurryTrunc.map · cited by 3Trunc.mapSemiquot.bind · cited by 2Semiquot.bindFunction.Embedding.truncOfCardLE · cited by 1Embedding.truncOfCardLEFintype.truncEquivOfCardEq · cited by 1Fintype.truncEquivOfCardEqFintype.truncRecEmptyOption · cited by 1Fintype.truncRecEmptyOpti…Encodable.fintypePi · cited by 0Encodable.fintypePiTrunc · cited by 39TruncTrunc.liftOn · cited by 0Trunc.liftOnTrunc.bindCITED BYCITES

Cites2

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

Cited by9

Results whose statement or proof uses this declaration.