iInter — Mathlib

English

If each set in a family is absolutely convex, their intersection is absolutely convex.

Русский

Если каждое множество в семье абсолютно выпукло, их пересечение тоже абсолютно выпукло.

LaTeX

$$$\\forall S,\\ AbsConvex(𝕜, S)\\Rightarrow AbsConvex(𝕜, \\bigcap S)$$$

Lean4

theorem iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, AbsConvex 𝕜 (s i)) : AbsConvex 𝕜 (⋂ i, s i) :=
  sInter_range s ▸ AbsConvex.sInter <| forall_mem_range.2 h

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