iUnion_eq_if — Mathlib

English

The union over h of p of s is equal to the conditional set: if p then the union is s else the empty set.

Русский

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

LaTeX

$$$\\bigcup_{h : p} s = \\text{if } p \\text{ then } s \\text{ else } \\emptyset$$$

Lean4

theorem iUnion_eq_if {p : Prop} [Decidable p] (s : Set α) : ⋃ _ : p, s = if p then s else ∅ :=
  iSup_eq_if _

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