tangentConeAt_closure — Mathlib

English

The tangent cone is stable under taking closures: tangentConeAt(𝕜, closure(s), x) = tangentConeAt(𝕜, s, x).

Русский

Касательный конус сохраняется при замыкании: tangentConeAt(𝕜, closure(s), x) = tangentConeAt(𝕜, s, x).

LaTeX

$$$\\operatorname{tangentCone}_{\\mathbb{k}}(\\overline{s}, x) = \\operatorname{tangentCone}_{\\mathbb{k}}(s, x)$$$

Lean4

@[simp]
theorem tangentConeAt_closure : tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x :=
  by
  refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)
  rintro y ⟨c, d, ds, ctop, clim⟩
  obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have : ∀ᶠ n in atTop, ∃ d', x + d' ∈ s ∧ dist (c n • d n) (c n • d') < u n :=
    by
    filter_upwards [ctop.eventually_gt_atTop 0, ds] with n hn hns
    rcases Metric.mem_closure_iff.mp hns (u n / ‖c n‖) (div_pos (u_pos n) hn) with ⟨y, hys, hy⟩
    refine ⟨y - x, by simpa, ?_⟩
    rwa [dist_smul₀, ← dist_add_left x, add_sub_cancel, ← lt_div_iff₀' hn]
  simp only [Filter.skolem, eventually_and] at this
  rcases this with ⟨d', hd's, hd'⟩
  exact
    ⟨c, d', hd's, ctop,
      clim.congr_dist (squeeze_zero' (.of_forall fun _ ↦ dist_nonneg) (hd'.mono fun _ ↦ le_of_lt) u_lim)⟩

Похожие утверждения