posTangentConeAt_mono — Mathlib

English

As s grows (s ⊆ t), the positive tangent cone at a is monotone: posTangentConeAt(s,a) ⊆ posTangentConeAt(t,a).

Русский

При расширении множества s ⊆ t положительный касательный конус в точке a увеличивается монотонно: posTangentConeAt(s,a) ⊆ posTangentConeAt(t,a).

LaTeX

$$$ s \\subseteq t \\quad\\Rightarrow\\quad posTangentConeAt(s,a) \\subseteq posTangentConeAt(t,a) $$$

Lean4

theorem posTangentConeAt_mono : Monotone fun s => posTangentConeAt s a :=
  by
  rintro s t hst y ⟨c, d, hd, hc, hcd⟩
  exact ⟨c, d, mem_of_superset hd fun h hn => hst hn, hc, hcd⟩

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