prod — Mathlib

English

Let s ⊆ E and t ⊆ F be convex subsets. Then their Cartesian product s × t is convex in E × F.

Русский

Пусть s ⊆ E и t ⊆ F являются выпуклыми множествами. Тогда их декартово произведение s × t выпукло в E × F.

LaTeX

$$$\Convex 𝕜 s \to \Convex 𝕜 t \to \Convex 𝕜 (s \times t)$$$

Lean4

theorem prod {s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ×ˢ t) := fun _ hx =>
  (hs hx.1).prod (ht hx.2)

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