exists_sUnion — Mathlib

English

There exists an x in ⋃₀ S with property p x if and only if there exists some s ∈ S and some x ∈ s with p x.

Русский

Существует x в ⋃₀ S такое, что p x, если и только если существует некоторое s ∈ S и x ∈ s с свойством p x.

LaTeX

$$$(\\exists x \\in \\bigcup_0 S,\np(x)) \\iff \\exists s \\in S, \\exists x \\in s, p(x)$$$

Lean4

theorem exists_sUnion {S : Set (Set α)} {p : α → Prop} : (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x := by
  simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]

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