posTangentConeAt_univ — Mathlib

English

The positive tangent cone at any a in the whole space equals the whole space.

Русский

Положительный касательный конус в любой точке a для всего пространства равен всему пространству.

LaTeX

$$$ posTangentConeAt univ a = univ $$$

Lean4

@[simp]
theorem posTangentConeAt_univ : posTangentConeAt univ a = univ :=
  eq_univ_of_forall fun _ => mem_posTangentConeAt_of_segment_subset (subset_univ _)

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