Theorems · Theorem · real analysis

isSeparable_range_derivWithin

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [TopologicalSpace.SeparableSpace 𝕜] (f : 𝕜 → F) (s : Set 𝕜),
  TopologicalSpace.IsSeparable (Set.range (derivWithin f s))

Defined in: Mathlib.Analysis.Calculus.Deriv.Slope
Cited by: 1 results in Mathlib
Foundations: Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NormedAddCommGroup NormedSpace TopologicalSpace.SeparableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

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
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
NontriviallyNormedFieldstatement and proof · cited by 8,742
Set.rangestatement · cited by 4,705
closureproof · cited by 1,254
Set.Countableproof · cited by 545
derivWithinstatement · cited by 258
TopologicalSpace.SeparableSpacestatement and proof · cited by 109
TopologicalSpace.IsSeparablestatement · cited by 51
Set.Countable.imageproof · cited by 47
Set.inter_eq_self_of_subset_rightproof · cited by 39

Cited by1

Results whose statement or proof uses this declaration.

isSeparable_range_derivproof · cited by 1