Theorems · Theorem · global analysis
uniqueDiffWithinAt_Iio
∀ (a : ℝ), UniqueDiffWithinAt ℝ (Set.Iio a) a
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Set.Nonemptyproof · cited by 2,627
- Set.Iiostatement · cited by 1,166
- UniqueDiffWithinAtstatement · cited by 252
- convex_Iioproof · cited by 6
- closure_Iioproof · cited by 5
- uniqueDiffWithinAt_convexproof · cited by 4
- interior_Iioproof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interiorproof · cited by 2
- InformationTheory.leftDeriv_klFunproof · cited by 1
- Real.leftDeriv_mul_logproof · cited by 0
- uniqueDiffWithinAt_Iicproof · cited by 0