Mathlib Map

Theorems · Definition · logic and foundations

Part.none

{α : Type u_1} → Part α

The none value in Part has a False domain and an empty function.

Defined in
Mathlib.Data.Part
Cited by
36 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.

Primrec.to_comp · cited by 40Primrec.to_compPart.ofOption · cited by 33Part.ofOptionPartrec.comp · cited by 12Partrec.compPartrec.bind · cited by 10Partrec.bindPart.bind_none · cited by 9Part.bind_noneComputable.ofOption · cited by 7Computable.ofOptionPart.eq_none_iff · cited by 6Part.eq_none_iffPart.map_none · cited by 5Part.map_noneComputable.pair · cited by 5Computable.pairPart.ωSup · cited by 4Part.ωSupPartrec.rfind · cited by 4Partrec.rfindPartrec.nat_rec · cited by 3Partrec.nat_recPartrec.none · cited by 3Partrec.nonePart.assert_neg · cited by 2Part.assert_negPart.eq_none_iff' · cited by 2Part.eq_none_iff'Part · cited by 325PartPart.noneCITED BYCITES

Cites1

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

  • Partstatement · cited by 325

Cited by38

Results whose statement or proof uses this declaration.