tangentConeAt_mono — Mathlib

English

If s ⊆ t, then the tangent cone at x relative to s is contained in the tangent cone at x relative to t.

Русский

Если s ⊆ t, то касательный конус к s в точке x вложен в касательный конус к t в точке x.

LaTeX

$$$s\subseteq t \Rightarrow tangentConeAt 𝕜 s x \subseteq tangentConeAt 𝕜 t x$$$

Lean4

@[gcongr]
theorem tangentConeAt_mono (h : s ⊆ t) : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x :=
  by
  rintro y ⟨c, d, ds, ctop, clim⟩
  exact ⟨c, d, mem_of_superset ds fun n hn => h hn, ctop, clim⟩

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