Theorems · Theorem · global analysis

subset_tangentConeAt_prod_left

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {x : E} {s : Set E}
  {y : F} {t : Set F}, y ∈ closure t → ⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

The tangent cone of a product contains the tangent cone of its left factor.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModuleTopologicalSpaceContinuousAddContinuousConstSMulAddCommGroupModuleTopologicalSpaceContinuousAddContinuousConstSMul