finite_iUnion_left_iff — Mathlib

English

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

Русский

Для конечного индекса I и семейства множеств s_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

theorem finite_iUnion_left_iff {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set X} {t : Set X} :
    AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t := by
  induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hI => rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]

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