Theorems · Definition · global analysis

tangentConeAt

(R : Type u_1) → {E : Type u_2} → [AddCommGroup E] → [SMul R E] → [TopologicalSpace E] → Set E → E → Set E

The set of all tangent directions to the set s at the point x. A point y belongs to the tangent cone of s at x iff there exist a family of scalars c n, a family of vectors d n, and a nontrivial filter in the index type such that - d n → 0 along the filter; - x + d n ∈ s eventually along the filter; - c n • d n → y along the filter, The actual definition is given in terms of cluster points of a filter, see mem_tangentConeAt_of_seq and exists_fun_of_mem_tangentConeAt for the two implications unfolding this definition in more convenient way. In a space with first countable topology, one can assume that the index type is ℕ and the filter is atTop, but the definition we use is more useful without that assumption.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Defs

Cited by

54 results in Mathlib

Foundations

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

Assumes

AddCommGroupSMulTopologicalSpace