convexJoin_mono_left

Mathlib.Analysis.Convex.Join

URI: https://scilib.ai/kg/mathlib#convexJoin_mono_left

English

If s1 ⊆ s2 then convexJoin 𝕜 s1 t ⊆ convexJoin 𝕜 s2 t.

Русский

Если s1 ⊆ s2, то convexJoin 𝕜 s1 t ⊆ convexJoin 𝕜 s2 t.

LaTeX

$$$ s_1 \subseteq s_2 \rightarrow convexJoin 𝕜 s_1 t \subseteq convexJoin 𝕜 s_2 t $$$

Lean4

theorem convexJoin_mono_left (hs : s₁ ⊆ s₂) : convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t :=
  convexJoin_mono hs Subset.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru