sInter — Mathlib

English

If the index type is a Subsingleton (i.e., has at most one element), then the union over i of s i is finite iff every s i is finite.

Русский

Если индексный тип является Subsingleton (не более одного элемента), то объединение ⋃ i s i конечно тогда и только тогда, когда каждый s i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\bigcup_{i} s(i)\\right) \\;\\iff\\; \\forall i, \\operatorname{Finite}(s(i))$$$

Lean4

theorem sInter {α : Type*} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) : (⋂₀ s).Finite :=
  hf.subset (sInter_subset_of_mem ht)

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