Mathlib Map

Theorems · Theorem · logic and foundations

Part.get_mem

∀ {α : Type u_1} {o : Part α} (h : o.Dom), o.get h ∈ o
Defined in
Mathlib.Data.Part
Cited by
6 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Nat.rfindOpt_dom · cited by 2Nat.rfindOpt_domPFun.preimage_eq · cited by 2PFun.preimage_eqPart.Dom.bind · cited by 1Dom.bindPart.ne_none_iff · cited by 1Part.ne_none_iffPFun.preimage_asSubtype · cited by 0PFun.preimage_asSubtypePFun.asSubtype_eq_of_mem · cited by 0PFun.asSubtype_eq_of_memPart · cited by 325PartPart.Dom · cited by 145Part.DomPart.get · cited by 77Part.getPart.get_memCITED 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.getstatement · cited by 77

Cited by6

Results whose statement or proof uses this declaration.