Theorems · Theorem · logic and foundations
Set.mem_ofPred_eq
∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ {y | p y}) = p x- Defined in
- Mathlib.Data.Set.Operations
- Cited by
- 122 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 9 definitions · uses no axioms
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 · cited by 53,352
- Set.ofPredstatement · cited by 6,101
Cited by122
Results whose statement or proof uses this declaration.
- MeasureTheory.lintegral_eq_zero_iff'proof · cited by 16
- Metric.isBounded_iffproof · cited by 15
- Metric.thickening_subset_cthickeningproof · cited by 12
- SimpleGraph.chromaticNumber_le_iff_colorableproof · cited by 10
- MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrictproof · cited by 6
- ProbabilityTheory.Kernel.indep_bot_rightproof · cited by 5
- isJacobsonRing_iff_prime_eqproof · cited by 5
- MeasureTheory.Measure.sub_applyproof · cited by 5
- MeasureTheory.TendstoInMeasure.exists_seq_tendsto_aeproof · cited by 5
- image_monotone_setOfPred_minimalproof · cited by 5
- PrimeSpectrum.mem_vanishingIdealproof · cited by 4
- MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurableproof · cited by 4