Mathlib Map

Theorems · Theorem · order theory

Set.empty_sdiff

∀ {α : Type u_1} (s : Set α), ∅ \ s = ∅
Defined in
Mathlib.Order.BooleanAlgebra.Set
Cited by
9 results in Mathlib
Foundations
Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.ite_empty_right · cited by 5Set.ite_empty_rightStieltjesFunction.length_empty · cited by 3StieltjesFunction.length_…MeasureTheory.OuterMeasure.boundedBy_caratheodory · cited by 2OuterMeasure.boundedBy_ca…Matroid.delete_loops_eq · cited by 1Matroid.delete_loops_eqMeasureTheory.Measure.addHaar_sphere_of_ne_zero · cited by 1Measure.addHaar_sphere_of…mem_map_indicator_ae_iff_of_zero_notMem · cited by 1mem_map_indicator_ae_iff_…Set.empty_diff · cited by 0Set.empty_diffStieltjesFunction.outer_trim · cited by 0StieltjesFunction.outer_t…MeasureTheory.OuterMeasure.top_caratheodory · cited by 0OuterMeasure.top_caratheo…Set · cited by 53352Setbot_sdiff · cited by 5bot_sdiffSet.empty_sdiffCITED BYCITES

Cites2

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

  • Setstatement and proof · cited by 53,352
  • bot_sdiffproof · cited by 5

Cited by9

Results whose statement or proof uses this declaration.