finset_iUnion_left_iff — Mathlib

English

For a finite index set I, the separation of the union over I with t is equivalent to the separations of each s_i with t.

Русский

Для фиксированного конечного множества индексов I верно: разнесённость ⋃_{i∈I} s_i относительно t эквивалентна …

LaTeX

$$$ \text{AreSeparated}(\bigcup_{i∈I} s_i, t) \iff \forall i∈I, \text{AreSeparated}(s_i, t) $$$

Lean4

@[simp]
theorem finset_iUnion_left_iff {ι : Type*} {I : Finset ι} {s : ι → Set X} {t : Set X} :
    AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t :=
  finite_iUnion_left_iff I.finite_toSet

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