English
If iSupIndep holds for A over s, then the family i ↦ (A i).comap (⨆ i∈s, A i).subtype is internal.
Русский
Если выполняется iSupIndep для A над множеством s, то семейство i ↦ (A i).comap (⨆ i∈s, A i).subtype является внутренним.
LaTeX
$$$IsInternal\Big(\lambda i:\, s \mapsto (A i).comap (\bigvee_{k\in s} A_k).subtype\Big)$$$
Lean4
theorem ofList_dProd {α} (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
of A _ (l.dProd fι fA) = (l.map fun a => of A (fι a) (fA a)).prod := by
induction l with
| nil => simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl
| cons head tail =>
rename_i ih
simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
rw [DirectSum.of_mul_of (fA head)]
rfl
