iUnion_eq_dif — Mathlib

English

The union over h : p of s h equals the dependent conditional s h if p; otherwise it is empty.

Русский

Объединение по h : p множества s(h) равно зависимому условному множеству s(h) при p; иначе пустое множество.

LaTeX

$$$\\bigcup_{h : p} s(h) = \\begin{cases} s(h), & h : p \\\\ \\\\emptyset, & \\text{ otherwise} \\end{cases}$$$

Lean4

theorem iUnion_eq_dif {p : Prop} [Decidable p] (s : p → Set α) : ⋃ h : p, s h = if h : p then s h else ∅ :=
  iSup_eq_dif _

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