Theorems · Theorem
Function.sometimes_spec
∀ {p : Prop} {α : Sort u_1} [inst : Nonempty α] (P : α → Prop) (f : p → α) (a : p), P (f a) → P (Function.sometimes f)- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 84 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Nonempty
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.
- Function.sometimesstatement · cited by 86
- Function.sometimes_eqproof · cited by 1
Cited by84
Results whose statement or proof uses this declaration.
- IsLindelof.elim_countable_subcoverproof · cited by 10
- IsCompact.disjoint_nhdsSet_leftproof · cited by 6
- HasDerivAt.lhopital_zero_right_on_Iooproof · cited by 5
- MonotoneOn.countable_setOfPred_two_preimagesproof · cited by 5
- MeasureTheory.measure_null_of_locally_nullproof · cited by 5
- Polynomial.splits_iff_exists_multiset'proof · cited by 4
- Set.Countable.isLindelof_biUnionproof · cited by 4
- BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filterproof · cited by 3
- Filter.map_atTop_eq_of_gc_preorderproof · cited by 3
- countable_image_lt_image_Ioi_withinproof · cited by 3
- countable_setOfPred_covBy_rightproof · cited by 3
- countable_setOfPred_isolated_right_withinproof · cited by 3