sInter — Mathlib

English

Let S be a finite collection of subsets of X, and each s ∈ S is retrocompact. Then their intersection ⋂₀ S is retrocompact.

Русский

Пусть S — конечная совокупность подмножеств X, и каждое s ∈ S ретрокомпактно. Тогда пересечение всех элементов S, ⋂₀ S, ретрокомпактно.

LaTeX

$$IsRetrocompact (⋂₀ S)$$

Lean4

theorem sInter {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) : IsRetrocompact (⋂₀ S) :=
  infClosed_isRetrocompact.sInf_mem hS .univ hS'

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