convexJoin_subset — Mathlib

English

If s ⊆ u and t ⊆ u and u is convex, then convexJoin 𝕜 s t ⊆ u.

Русский

Если s ⊆ u и t ⊆ u и u выпуклая, то convexJoin 𝕜 s t ⊆ u.

LaTeX

$$$ s \subseteq u \rightarrow t \subseteq u \rightarrow \operatorname{Convex} 𝕜 u \rightarrow convexJoin 𝕜 s t \subseteq u $$$

Lean4

theorem convexJoin_subset (hs : s ⊆ u) (ht : t ⊆ u) (hu : Convex 𝕜 u) : convexJoin 𝕜 s t ⊆ u :=
  iUnion₂_subset fun _x hx => iUnion₂_subset fun _y hy => hu.segment_subset (hs hx) (ht hy)

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