Theorems · Theorem · global analysis

mem_tangentConeAt_iff_exists_seq

∀ {R : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E]
  [FirstCountableTopology E] {s : Set E} {x y : E},
  y ∈ tangentConeAt R s x ↔
    ∃ c d,
      Filter.Tendsto d Filter.atTop (nhds 0) ∧
        (∀ᶠ (n : ℕ) in Filter.atTop, x + d n ∈ s) ∧ Filter.Tendsto (fun n => c n • d n) Filter.atTop (nhds y)

In a vector space with first countable topology, a vector y belongs to tangentConeAt 𝕜 s x if and only if there exist sequences c n and d n such that - d n tends to zero as n → ∞; - x + d n ∈ s for sufficiently large n; - c n • d n tends to y as n → ∞. See mem_tangentConeAt_of_seq and exists_fun_of_mem_tangentConeAt for versions of two implications of this theorem that don't assume first countable topology.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Seq

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupSMulTopologicalSpaceFirstCountableTopology