sub_mem_posTangentConeAt_of_segment_subset

English

If a segment from x to y lies in s, then y − x lies in posTangentConeAt s x.

Русский

Если отрезок от x до y лежит в s, то y−x принадлежит posTangentConeAt s x.

LaTeX

$$$\\text{segment}(x,y)\\subseteq s \\Rightarrow y-x\\in posTangentConeAt(s,x)$$$

Lean4

theorem sub_mem_posTangentConeAt_of_segment_subset (h : segment ℝ x y ⊆ s) : y - x ∈ posTangentConeAt s x :=
  mem_posTangentConeAt_of_segment_subset <| by rwa [add_sub_cancel]

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