finset_iUnion_right_iff — Mathlib

English

Symmetric statement to the left version: AreSeparated(s, ⋃_{i∈I} t_i) iff ∀ i∈I, AreSeparated(s, t_i).

Русский

Симметрично к левому: AreSeparated(s, ⋃_{i∈I} t_i) эквивалентно ∀ i∈I, AreSeparated(s, t_i).

LaTeX

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

Lean4

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

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