sInter_mem — Mathlib

English

For a finite family s of sets, the intersection over all sets in s belongs to f iff every set in s belongs to f.

Русский

Для конечной коллекции множеств s пересечение всех множеств из s принадлежит фильтру f тогда и только тогда, когда каждое множество из s принадлежит f.

LaTeX

$$$s\\in f \\Rightarrow \\bigcap_{U\\in s} U \\in f \\iff \\forall U \\in s, U \\in f$$$

Lean4

@[simp]
theorem sInter_mem {s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f := by
  rw [sInter_eq_biInter, biInter_mem hfin]

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