Mathlib Map

Theorems · Theorem · logic and foundations

Part.sdiff_mem_sdiff

∀ {α : Type u_1} [inst : SDiff α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma \ mb ∈ a \ b
Defined in
Mathlib.Data.Part
Cited by
0 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext, Quot.sound
Assumes
SDiff
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Part · cited by 325PartPart.sdiff_mem_sdiffCITED BYCITES

Cites1

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

  • Partstatement and proof · cited by 325

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.