sInter — Mathlib

English

If a collection S of subsets of E consists entirely of balanced sets, then the intersection of all of them is balanced.

Русский

Если множество S состоит из подмножеств пространства E, каждое из которых сбалансировано, то пересечение всех них сбалансировано.

LaTeX

$$$\Big( \forall s\in S, \text{Balanced}_{\mathfrak{k}}(s) \Big) \Rightarrow \text{Balanced}_{\mathfrak{k}}\Big( \bigcap S \Big)$$$

Lean4

theorem sInter {S : Set (Set E)} (h : ∀ s ∈ S, Balanced 𝕜 s) : Balanced 𝕜 (⋂₀ S) := fun _ _ =>
  (smul_set_sInter_subset ..).trans (fun _ _ => by aesop)

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