balanced_iInter — Mathlib

English

If a family of sets {f(i)} indexed by i is such that every f(i) is balanced, then the intersection over i is balanced.

Русский

Если множество семей f(i) имеет для каждого i сбалансированное множество, то пересечение по всем i сбалансировано.

LaTeX

$$$\forall i, \text{Balanced}_{\mathfrak{k}}(f(i)) \Rightarrow \text{Balanced}_{\mathfrak{k}}\Big( \bigcap_i f(i) \Big)$$$

Lean4

theorem balanced_iInter {f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋂ i, f i) := fun _a ha =>
  (smul_set_iInter_subset _ _).trans <| iInter_mono fun _ => h _ _ ha

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