coe_biUnion — Mathlib

English

The set corresponding to the biUnion of a Finset is the union, over elements of the index set, of the corresponding sets.

Русский

Множество, соответствующее biUnion, есть объединение по элементам индекса и соответствующим множествам.

LaTeX

$$$(s.biUnion t).toSet = \\bigcup_{x \\in s} t x$$$

Lean4

@[simp, norm_cast]
theorem coe_biUnion : (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x := by
  simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, mem_coe]

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