Mathlib Map

Theorems · Theorem · logic and foundations

Part.dom_iff_mem

∀ {α : Type u_1} {o : Part α}, o.Dom ↔ ∃ y, y ∈ o
Defined in
Mathlib.Data.Part
Cited by
6 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Part.Fix.mem_iff · cited by 2Fix.mem_iffPFun.preimage_subset_dom · cited by 1PFun.preimage_subset_domPFun.dom_iff_graph · cited by 1PFun.dom_iff_graphNat.mem_rfind · cited by 0Nat.mem_rfindPart.eq_of_mem · cited by 0Part.eq_of_memNat.rfind_min' · cited by 0Nat.rfind_min'Part · cited by 325PartPart.Dom · cited by 145Part.DomPart.dom_iff_memCITED 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 and proof · cited by 145

Cited by6

Results whose statement or proof uses this declaration.