English
If hC is a SetRing and S is a finite index set with each s(i) ∈ C for i ∈ S, then the union over i ∈ S of s(i) lies in C.
Русский
Если hC — множество колец, и S — конечный индекс, причем каждый s(i) ∈ C, тогда объединение по i ∈ S принадлежит C.
LaTeX
$$$\text{If } hC\text{ is a SetRing and } S\text{ finite}, \ \forall i\in S:\ s(i)\in C \implies \bigcup_{i\in S} s(i)\in C.$$$
Lean4
theorem biUnion_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} (S : Finset ι) (hs : ∀ n ∈ S, s n ∈ C) :
⋃ i ∈ S, s i ∈ C := by
classical
induction S using Finset.induction with
| empty => simp [hC.empty_mem]
| insert i S _ h =>
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
refine hC.union_mem (hs i (mem_insert_self i S)) ?_
exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))
