finite_biUnion_mem_iff — Mathlib

English

Let f be an ultrafilter on α, is a finite set, and s(i) ⊆ α for i in is. Then the union ⋃ i∈is s(i) belongs to f if and only if ∃ i∈is with s(i) ∈ f.

Русский

Пусть f – ульрафильтр на α, is – конечное множество индексов, и s(i) ⊆ α. Тогда ⋃ i∈is s(i) ∈ f тогда и только тогда, когда ∃ i∈is such that s(i) ∈ f.

LaTeX

$$$\\bigcup_{i\\in is} s(i) \\in f \\iff \\exists i\\in is,\\ s(i)\\in f$$

Lean4

theorem finite_biUnion_mem_iff {is : Set β} {s : β → Set α} (his : is.Finite) :
    (⋃ i ∈ is, s i) ∈ f ↔ ∃ i ∈ is, s i ∈ f := by
  simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), exists_mem_image]

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