Theorems · Theorem · global analysis

UniqueDiffWithinAt.of_closure

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E],
  UniqueDiffWithinAt 𝕜 (closure s) x → UniqueDiffWithinAt 𝕜 s x

Alias of the forward direction of uniqueDiffWithinAt_closure.

Defined in: Mathlib.Analysis.Calculus.TangentCone.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommGroup Module TopologicalSpace ContinuousAdd ContinuousConstSMul

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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
TopologicalSpacestatement and proof · cited by 24,529
Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommGroupstatement and proof · cited by 12,871
closurestatement · cited by 1,254
ContinuousConstSMulstatement and proof · cited by 832
ContinuousAddstatement and proof · cited by 777
UniqueDiffWithinAtstatement · cited by 252
uniqueDiffWithinAt_closureproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

UniqueDiffWithinAt.mono_closureproof · cited by 1