Mathlib Map

Theorems · Theorem · logic and foundations

Part.right_dom_of_sdiff_dom

∀ {α : Type u_1} [inst : SDiff α] {a b : Part α}, (a \ b).Dom → b.Dom
Defined in
Mathlib.Data.Part
Cited by
1 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
SDiff
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Part.sdiff_get_eq · cited by 0Part.sdiff_get_eqPart · cited by 325PartPart.Dom · cited by 145Part.DomPart.right_dom_of_sdiff_domCITED 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 by1

Results whose statement or proof uses this declaration.