Mathlib Map

Theorems · Theorem · logic and foundations

Part.mem_map

∀ {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {a : α}, a ∈ o → f a ∈ Part.map f o
Defined in
Mathlib.Data.Part
Cited by
2 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.map_some · cited by 27Part.map_somePart.mem_map_iff · cited by 5Part.mem_map_iffPart · cited by 325PartPart.Dom · cited by 145Part.DomPart.map · cited by 65Part.mapPart.mem_mapCITED 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.Domproof · cited by 145
  • Part.mapstatement and proof · cited by 65

Cited by2

Results whose statement or proof uses this declaration.