Theorems · Theorem · logic and foundations
Set.ofPred_subset_ofPred_of_imp
∀ {α : Type u} {p q : α → Prop}, (∀ (a : α), p a → q a) → {a | p a} ⊆ {a | q a}Alias of the reverse direction of Set.ofPred_subset_ofPred.
- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
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 · cited by 53,352
- Set.ofPredstatement · cited by 6,101
- Set.ofPred_subset_ofPredproof · cited by 3
Cited by22
Results whose statement or proof uses this declaration.
- gauge_monoproof · cited by 4
- MeasureTheory.tendstoInMeasure_of_ne_topproof · cited by 4
- rieszContentAux_monoproof · cited by 3
- MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_leproof · cited by 2
- TopologicalSpace.Compacts.continuous_prodproof · cited by 2
- MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegralproof · cited by 2
- UniformSpace.hausdorff.isClosed_setOfPred_totallyBoundedproof · cited by 2
- TopologicalSpace.Compacts.isPreconnected_nonempty_subsetsproof · cited by 2
- MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_innerproof · cited by 2
- MeasureTheory.upcrossingsBefore_monoproof · cited by 1
- MeasureTheory.unifIntegrable_ofproof · cited by 1
- MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurableproof · cited by 1