tangentConeAt_univ — Mathlib

English

The tangent cone to the whole space at any point is the whole space itself.

Русский

Касательный конус к всей пространства в любой точке совпадает с всем пространством.

LaTeX

$$$tangentConeAt 𝕜 Set.univ x = Set.univ$$$

Lean4

@[simp]
theorem tangentConeAt_univ : tangentConeAt 𝕜 univ x = univ :=
  let ⟨_r, hr₀, hr⟩ := exists_norm_lt_one 𝕜
  eq_univ_of_forall fun _ ↦
    mem_tangentConeAt_of_pow_smul (norm_pos_iff.1 hr₀) hr <| Eventually.of_forall fun _ ↦ mem_univ _

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