iInter₂ — Mathlib

English

If every j-th family member is AbsConvex, then the double index intersection is AbsConvex.

Русский

Если каждый двойной индексный элемент семейства AbsConvex, то двойной пересекающий индекс также AbsConvex.

LaTeX

$$$\\forall i\\,\\forall j, AbsConvex 𝕜 (f_i_j)\\Rightarrow AbsConvex 𝕜 (\\bigcap_i\\bigcap_j f_i_j)$$$

Lean4

theorem iInter₂ {ι : Sort*} {κ : ι → Sort*} {f : ∀ i, κ i → Set E} (h : ∀ i j, AbsConvex 𝕜 (f i j)) :
    AbsConvex 𝕜 (⋂ (i) (j), f i j) :=
  AbsConvex.iInter fun _ => (AbsConvex.iInter fun _ => h _ _)

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