Mathlib Map

Theorems · Theorem · logic and foundations

Set.eq_empty_of_isEmpty

∀ {α : Type u} (s : Set α) [IsEmpty ↑s], s = ∅
Defined in
Mathlib.Data.Set.Basic
Cited by
21 results in Mathlib
Foundations
Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
IsEmpty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsCoveringMapOn.of_isEmpty · cited by 2IsCoveringMapOn.of_isEmptyFinsupp.lmapDomain_supported · cited by 2Finsupp.lmapDomain_suppor…measurableSet_bddAbove_range · cited by 2measurableSet_bddAbove_ra…Besicovitch.exist_disjoint_covering_families · cited by 2Besicovitch.exist_disjoin…Set.encard_image_le · cited by 2Set.encard_image_leDynamics.IsDynCoverOf.preimage · cited by 1IsDynCoverOf.preimageStieltjesFunction.isFiniteMeasure · cited by 1StieltjesFunction.isFinit…IsMaxAntichain.isEmpty_iff · cited by 1IsMaxAntichain.isEmpty_iffIsMaxChain.isEmpty_iff · cited by 1IsMaxChain.isEmpty_iffMeasureTheory.exists_isCompact_closure_measure_compl_lt · cited by 1MeasureTheory.exists_isCo…MeasureTheory.Measure.apply_eq_zero_of_isEmpty · cited by 1Measure.apply_eq_zero_of_…Set.univ_set_of_isEmpty · cited by 1Set.univ_set_of_isEmptyeVariationOn.comp_eq_of_antitoneOn · cited by 1eVariationOn.comp_eq_of_a…eVariationOn.comp_eq_of_monotoneOn · cited by 1eVariationOn.comp_eq_of_m…Besicovitch.exist_finset_disjoint_balls_large_measure · cited by 1Besicovitch.exist_finset_…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemIsEmpty · cited by 759IsEmptySet.eq_empty_of_isEmptyCITED BYCITES

Cites3

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
  • Set.Elemstatement and proof · cited by 7,166
  • IsEmptystatement and proof · cited by 759

Cited by21

Results whose statement or proof uses this declaration.