Mathlib Map

Theorems · Definition · logic and foundations

Part.get

{α : Type u} → (self : Part α) → self.Dom → α

Extract a value from a partial value given a proof of Dom

Defined in
Mathlib.Data.Part
Cited by
77 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Part.bind · cited by 70Part.bindPart.map · cited by 65Part.mapPart.ext · cited by 24Part.extPart.eq_some_iff · cited by 17Part.eq_some_iffPart.toOption · cited by 16Part.toOptionPFun.fix · cited by 16PFun.fixPart.assert · cited by 10Part.assertPFun.prodMap · cited by 7PFun.prodMapPFun.fixInduction · cited by 6PFun.fixInductionPFun.fn · cited by 6PFun.fnPFun.mem_fix_iff · cited by 6PFun.mem_fix_iffPart.ext' · cited by 6Part.ext'Part.get_mem · cited by 6Part.get_memPart.mem_map_iff · cited by 5Part.mem_map_iffPFun.prodLift · cited by 5PFun.prodLiftPart · cited by 325PartPart.Dom · cited by 145Part.DomPart.getCITED BYCITES

Cites2

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

  • Partstatement and proof · cited by 325
  • Part.Domstatement · cited by 145

Cited by93

Results whose statement or proof uses this declaration.