Theorems · Theorem · global analysis

mem_tangentConeAt_of_seq

∀ {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 α) [l.NeBot] (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

A special case of mem_tangentConeAt_of_frequently, which avoids Filter.Frequently.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Defs

Cited by

8 results in Mathlib

Foundations

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

Assumes

AddCommGroupSMulTopologicalSpaceFilter.NeBot