finite_iUnion_right_iff — Mathlib

English

For a finite index set I and a family t_i, the separation of s from the big union is equivalent to separations of s with each t_i.

Русский

Для конечного индекса I и семейства t_i разнесённость s относительно ⋃ i∈I t_i эквивалентна ...

LaTeX

$$$ \text{AreSeparated}(s, \bigcup_{i∈I} t_i) \iff \forall i∈I, \text{AreSeparated}(s,t_i) $$$

Lean4

theorem finite_iUnion_right_iff {ι : Type*} {I : Set ι} (hI : I.Finite) {s : Set X} {t : ι → Set X} :
    AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i) := by
  simpa only [@comm _ _ s] using finite_iUnion_left_iff hI

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