Theorems · Theorem · logic and foundations
Set.eq_empty_of_subset_empty
∀ {α : Type u} {s : Set α}, s ⊆ ∅ → s = ∅- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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
- Set.subset_empty_iffproof · cited by 40
Cited by15
Results whose statement or proof uses this declaration.
- Set.preimage_const_of_notMemproof · cited by 6
- Filter.not_isBoundedUnder_of_tendsto_atTopproof · cited by 4
- IsEvenlyCovered.of_preimage_eq_emptyproof · cited by 4
- NoBotOrder.lowerBounds_univproof · cited by 1
- NoTopOrder.upperBounds_univproof · cited by 1
- Interval.coe_sInfproof · cited by 1
- exists_of_linearIndepOn_of_finite_spanproof · cited by 1
- WithBot.preimage_coe_botproof · cited by 0
- balancedCore_emptyproof · cited by 0
- WithTop.preimage_coe_topproof · cited by 0
- iInter_Iio_of_not_bddBelow_rangeproof · cited by 0
- Filter.not_isBoundedUnder_of_tendsto_atBotproof · cited by 0