English
For a finite index set s and a family f : ι → Compacts α, the carrier of the join over s equals the finite union of carriers: ↑(s.sup f) = s.sup (i ↦ ↑(f i)).
Русский
Для конечного множества индексов s и семейства f : ι → Compacts α носитель объединения ∑ over s равен конечному объединению носителей: ↑(s.sup f) = s.sup (i ↦ ↑(f i)).
LaTeX
$$$\\forall {\\iota : Type*} {s : \\mathrm{Finset} \\iota} {f : \\iota → \\mathrm{Compacts}(\\alpha)},\\\\ (↑(s.sup f) : \\text{Set }\\alpha) = s.sup (fun i => ↑(f i))$$$
Lean4
@[simp]
theorem coe_finset_sup {ι : Type*} {s : Finset ι} {f : ι → Compacts α} : (↑(s.sup f) : Set α) = s.sup fun i => ↑(f i) :=
by
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
congr
