Mathlib Map

Theorems · Definition · logic and foundations

Part.toOption

{α : Type u_1} → (o : Part α) → [Decidable o.Dom] → Option α

Convert a Part α with a decidable domain to an option

Defined in
Mathlib.Data.Part
Cited by
16 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Decidable
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

partialFunToPointed · cited by 8partialFunToPointedPart.toFinset · cited by 5Part.toFinsetPart.mem_toOption · cited by 2Part.mem_toOptionPart.Dom.toOption · cited by 2Dom.toOptionPart.toOption_eq_none_iff · cited by 2Part.toOption_eq_none_iffDecidable.Partrec.const' · cited by 2Partrec.const'Part.toOption.congr_simp · cited by 1toOption.congr_simpPart.none_toOption · cited by 1Part.none_toOptionPart.of_toOption · cited by 1Part.of_toOptionPart.some_toOption · cited by 1Part.some_toOptionpartialFunEquivPointed_functor_map_toFun · cited by 0partialFunEquivPointed_fu…PFun.evalOpt · cited by 0PFun.evalOptPart.toOption_eq_none · cited by 0Part.toOption_eq_nonePart.toOption_eq_some_iff · cited by 0Part.toOption_eq_some_iffpartialFunToPointed_map · cited by 0partialFunToPointed_mapPart · cited by 325PartPart.Dom · cited by 145Part.DomPart.get · cited by 77Part.getPart.toOptionCITED BYCITES

Cites3

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 and proof · cited by 145
  • Part.getproof · cited by 77

Cited by20

Results whose statement or proof uses this declaration.