Theorems · Theorem · logic and foundations
Set.inter_univ
∀ {α : Type u} (a : Set α), a ∩ Set.univ = a- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 198 results in Mathlib
- Foundations
- Depth 21 from the axioms, rests on 128 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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.univstatement · cited by 3,945
- inf_top_eqproof · cited by 30
Cited by198
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.restrict_univproof · cited by 76
- MeasureTheory.measure_toMeasurableproof · cited by 53
- PartialEquiv.trans_reflproof · cited by 30
- IsOpen.isLocallyClosedproof · cited by 20
- OpenPartialHomeomorph.extend_sourceproof · cited by 17
- MeasureTheory.lintegral_iSupproof · cited by 16
- Set.prod_univproof · cited by 14
- ContMDiffWithinAt.mdifferentiableWithinAtproof · cited by 11
- MeasureTheory.Measure.fst_map_prodMk₀proof · cited by 9
- ProbabilityTheory.mgf_pos'proof · cited by 9
- mfderivWithin_eq_fderivWithinproof · cited by 8
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetproof · cited by 8