convexJoin_mono_right

Mathlib.Analysis.Convex.Join

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

English

If t1 ⊆ t2 then convexJoin 𝕜 s t1 ⊆ convexJoin 𝕜 s t2.

Русский

Если t1 ⊆ t2, то convexJoin 𝕜 s t1 ⊆ convexJoin 𝕜 s t2.

LaTeX

$$$ t_1 \subseteq t_2 \rightarrow convexJoin 𝕜 s t_1 \subseteq convexJoin 𝕜 s t_2 $$$

Lean4

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

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

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

Разделы

Аффилиация

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