convex_iInter₂ — Mathlib

English

If every s_i_j is convex, the double indexed intersection is convex.

Русский

Если все s_{i,j} выпуклы, то двойное индексированное пересечение выпукло.

LaTeX

$$$\forall i,j,\ \mathrm{Convex } 𝕜 (s_{i j}) \Rightarrow \mathrm{Convex } 𝕜 (\bigcap_i \bigcap_j s_{i j})$$$

Lean4

theorem convex_iInter₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, Convex 𝕜 (s i j)) :
    Convex 𝕜 (⋂ (i) (j), s i j) :=
  convex_iInter fun i => convex_iInter <| h i

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