forall_sUnion — Mathlib

English

Let S be a collection of sets and p a property on the base type. Then (forall x in ⋃₀ S, p x) is equivalent to (for all s in S, for all x in s, p x).

Русский

Пусть S — коллекция множеств, а p — свойство на базовом множестве. Тогда (для всех x, принадлежащих ⋃₀ S, верно p x) эквивалентно (для всех s в S и для всех x в s, верно p x).

LaTeX

$$$\\bigl( \\forall x \\in \\bigcup_0 S,\n p(x) \\bigr) \\iff \\forall s \\in S, \\forall x \\in s, p(x)$$$

Lean4

theorem forall_sUnion {S : Set (Set α)} {p : α → Prop} : (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x := by
  simp_rw [← iInf_Prop_eq, iInf_sUnion]

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