Theorems · Theorem · order theory
StrictMonoOn.mono
∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
StrictMonoOn f s → s₂ ⊆ s → StrictMonoOn f s₂- Defined in
- Mathlib.Data.Set.Monotone
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 6 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 and proof · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- StrictMonoOnstatement and proof · cited by 194
Cited by15
Results whose statement or proof uses this declaration.
- AkraBazziRecurrence.strictAntiOn_smoothingFnproof · cited by 4
- StrictMonoOn.strictConvexOn_of_derivproof · cited by 4
- StrictMonoOn.Iic_id_leproof · cited by 3
- ArchimedeanClass.mk_sumproof · cited by 2
- Continuous.strictMonoOn_of_inj_rigidityproof · cited by 1
- StrictMonoOn.exists_deriv_lt_slopeproof · cited by 1
- HahnEmbedding.Seed.baseEmbedding_posproof · cited by 1
- Nat.le_nthproof · cited by 1
- StrictMonoOn.exists_slope_lt_derivproof · cited by 1
- MulArchimedeanClass.mk_prodproof · cited by 0
- Real.image_log_Iocproof · cited by 0
- MeasureTheory.integral_comp_rpow_Ioi_of_pos'proof · cited by 0