convexJoin_comm

Mathlib.Analysis.Convex.Join

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

English

The join is symmetric: convexJoin 𝕜 s t = convexJoin 𝕜 t s.

Русский

Симметрия соединения: convexJoin 𝕜 s t = convexJoin 𝕜 t s.

LaTeX

$$$ convexJoin 𝕜 s t = convexJoin 𝕜 t s $$$

Lean4

theorem convexJoin_comm (s t : Set E) : convexJoin 𝕜 s t = convexJoin 𝕜 t s :=
  (iUnion₂_comm _).trans <| by simp_rw [convexJoin, segment_symm]

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

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

Разделы

Аффилиация

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