convexJoin_iUnion_right

Mathlib.Analysis.Convex.Join

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

← MathLib Explorer

English

convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i).

Русский

convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i).

LaTeX

$$$ convexJoin 𝕜 s (\bigcup_i t_i) = \bigcup_i convexJoin 𝕜 s (t_i) $$$

Lean4

@[simp]
theorem convexJoin_iUnion_right (s : Set E) (t : ι → Set E) : convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i) :=
  by simp_rw [convexJoin_comm s, convexJoin_iUnion_left]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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