Theorems · Theorem · global analysis

Filter.HasBasis.tangentConeAt_eq_biInter_closure

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E} {ι : Sort u_3} {p : ι → Prop} {U : ι → Set E},
  (nhds 0).HasBasis p U →
    tangentConeAt 𝕜 s x = ⋂ i, ⋂ (_ : p i), closure (Set.univ • (U i ∩ (fun x_2 => x + x_2) ⁻¹' s))

Defined in

Mathlib.Analysis.Calculus.TangentCone.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupSMulTopologicalSpace