Theorems · Theorem · global analysis

mem_tangentConeAt_of_frequently

∀ {R : Type u} {E : Type v} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x y : E} {α : Type u_1} (l : Filter α) (c : α → R) (d : α → E),
  Filter.Tendsto d l (nhds 0) →
    (∃ᶠ (n : α) in l, x + d n ∈ s) → Filter.Tendsto (fun n => c n • d n) l (nhds y) → y ∈ tangentConeAt R s x

Let c n be a family of scalars, d n be a family of vectors, and l be a filter such that - d n → 0 along l; - x + d n ∈ s frequently along l; - c n • d n → y along l. Then y belongs to the tangent cone of s at x. See also - mem_tangentConeAt_of_seq for a version assuming that x + d n ∈ s eventually along l. - exists_fun_of_mem_tangentConeAt for the other implication.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Defs

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupSMulTopologicalSpace