English
If x is in the closure of s, then the image of tangentConeAt(t, y) under the right injection lies in the tangent cone of the product s × t at (x, y).
Русский
Если x лежит в замыкании s, то образ касательного конуса правого компонента при внедрении справа входит в касательный конус произведения s × t в точке (x, y).
LaTeX
$$$\\operatorname{inr}_{\\mathbb{k}}(E,F)[\\operatorname{tangentCone}_{\\mathbb{k}}(t, y)] \\subseteq \\operatorname{tangentCone}_{\\mathbb{k}}(s \\times t)(x, y) \\quad (x \\in \\overline{s})$$$
Lean4
/-- The tangent cone of a product contains the tangent cone of its right factor. -/
theorem subset_tangentConeAt_prod_right {t : Set F} {y : F} (hs : x ∈ closure s) :
LinearMap.inr 𝕜 E F '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y) :=
by
rintro _ ⟨w, ⟨c, d, hd, hc, hy⟩, rfl⟩
have : ∀ n, ∃ d', x + d' ∈ s ∧ ‖c n • d'‖ < ((1 : ℝ) / 2) ^ n :=
by
intro n
rcases mem_closure_iff_nhds.1 hs _ (eventually_nhds_norm_smul_sub_lt (c n) x (pow_pos one_half_pos n)) with
⟨z, hz, hzs⟩
exact ⟨z - x, by simpa using hzs, 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
