finite_sUnion_mem_iff — Mathlib

English

For an ultrafilter f on α and a finite set s of subsets of α, the union ⋃₀ s belongs to f if and only if some member t of s belongs to f.

Русский

Для ульрафильтра f на α и конечно множества s ⊆ 2^α верно: ⋃₀ s ∈ f тогда и только тогда, когда существует t ∈ s такое, что t ∈ f.

LaTeX

$$$\\bigcup_{t\\in s} t \\in f \\iff \\exists t\\in s,\\ t\\in f$$

Lean4

theorem finite_sUnion_mem_iff {s : Set (Set α)} (hs : s.Finite) : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f := by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]

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