coe_disjiUnion — Mathlib

English

The coercion of disjiUnion to a set equals the union of the corresponding sets.

Русский

Переобразование disjiUnion в множество совпадает с объединением соответствующих множеств.

LaTeX

$$$ (s.disjiUnion t h : Set \\beta) = ⋃ x ∈ (s : Set \\alpha), t x $$$

Lean4

@[simp, norm_cast]
theorem coe_disjiUnion {h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x := by
  simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, mem_coe]

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