English
In 1D, AccPt implies tangentConeAt equals univ; specialized simp lemmas express this.
Русский
В 1D, AccPt равносильно тому, что tangentConeAt совпадает с единицей; упрощённые леммы формулируются как упрощение.
LaTeX
$$$\\text{tangentConeAt}_{\\mathbb{k}}(s, x) = \\operatorname{univ}$$$
Lean4
/-- The tangent cone at a non-isolated point in dimension 1 is the whole space. -/
theorem tangentConeAt_eq_univ {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (𝓟 s)) : tangentConeAt 𝕜 s x = univ :=
by
apply
eq_univ_iff_forall.2
(fun y ↦ ?_)
-- first deal with the case of `0`, which has to be handled separately.
rcases eq_or_ne y 0 with rfl | hy
·
exact
zero_mem_tangentCone
(mem_closure_iff_clusterPt.mpr hx.clusterPt)
/- Assume now `y` is a fixed nonzero scalar. Take a sequence `d n` tending to `0` such
that `x + d n ∈ s`. Let `c n = y / d n`. Then `‖c n‖` tends to infinity, and `c n • d n`
converges to `y` (as it is equal to `y`). By definition, this shows that `y` belongs to the
tangent cone. -/
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
exists_seq_strictAnti_tendsto (0 : ℝ)
have A n : ∃ y ∈ closedBall x (u n) ∩ s, y ≠ x := accPt_iff_nhds.mp hx _ (closedBall_mem_nhds _ (u_pos n))
choose v hv hvx using A
choose hvu hvs using hv
let d := fun n ↦ v n - x
have d_ne n : d n ≠ 0 := by simpa [d, sub_eq_zero] using hvx n
refine ⟨fun n ↦ y * (d n)⁻¹, d, .of_forall ?_, ?_, ?_⟩
· simpa [d] using hvs
· simp only [norm_mul, norm_inv]
apply (tendsto_const_mul_atTop_of_pos (by simpa using hy)).2
apply tendsto_inv_nhdsGT_zero.comp
simp only [nhdsWithin, tendsto_inf, tendsto_principal, mem_Ioi, norm_pos_iff, ne_eq, eventually_atTop, ge_iff_le]
have B (n : ℕ) : ‖d n‖ ≤ u n := by simpa [dist_eq_norm] using hvu n
refine ⟨?_, 0, fun n hn ↦ by simpa using d_ne n⟩
exact squeeze_zero (fun n ↦ by positivity) B u_lim
· convert tendsto_const_nhds (α := ℕ) (x := y) with n
simp [mul_assoc, inv_mul_cancel₀ (d_ne n)]
