Theorems · Theorem · global analysis

mapsTo_tangentConeAt_pi

∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)]
  [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} [inst_6 : DecidableEq ι]
  {i : ι},
  (∀ (j : ι), j ≠ i → x j ∈ closure (s j)) →
    Set.MapsTo (Pi.single i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)

The tangent cone of a product contains the tangent cone of each factor.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModuleTopologicalSpaceContinuousAddContinuousConstSMulDecidableEq