English
If y is in the closure of t, then the image of tangentConeAt(s, x) under the left injection is contained in the tangent cone of the product s × t at (x, y).
Русский
Если y лежит в замыкании t, то образ касательного конуса левого компонента при внедрении слева входит в касательный конус произведения s × t в точке (x, y).
LaTeX
$$$\\operatorname{inl}_{\\mathbb{k}}(E,F)[\\operatorname{tangentCone}_{\\mathbb{k}}(s, x)] \\subseteq \\operatorname{tangentCone}_{\\mathbb{k}}(s \\times t)(x, y) \\quad (y \\in \\overline{t})$$$
Lean4
/-- The tangent cone of a product contains the tangent cone of its left factor. -/
theorem subset_tangentConeAt_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) :
LinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y) :=
by
rintro _ ⟨v, ⟨c, d, hd, hc, hy⟩, rfl⟩
have : ∀ n, ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < ((1 : ℝ) / 2) ^ n :=
by
intro n
rcases mem_closure_iff_nhds.1 ht _ (eventually_nhds_norm_smul_sub_lt (c n) y (pow_pos one_half_pos n)) with
⟨z, hz, hzt⟩
exact ⟨z - y, by simpa using hzt, by simpa using hz⟩
choose d' hd' using this
refine ⟨c, fun n => (d n, d' n), ?_, hc, ?_⟩
· change ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
filter_upwards [hd] with n hn
simp [hn, (hd' n).1]
· apply Tendsto.prodMk_nhds hy _
refine squeeze_zero_norm (fun n => (hd' n).2.le) ?_
exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one
