English
If for every i the family s(i) is pairwise disjoint with respect to f(i), then the global Pi-structure over univ with s is pairwise disjoint with respect to the family (f i (I i)).
Русский
Если для каждого i семейство s(i) попарно непересекается относительно f(i), тогда глобальная структура Pi над одиничной степенью попарно непересекается относительно семейства f(i)(I(i)).
LaTeX
$$$$\text{If } \forall i, (s(i)).PairwiseDisjoint (f(i)) \text{ then } ((univ : Set ι).pi s).PairwiseDisjoint (\lambda I \to (univ : Set ι).pi (\lambda i, f i (I i))).$$$$
Lean4
theorem pairwiseDisjoint_pi {ι' α : ι → Type*} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)}
(hs : ∀ i, (s i).PairwiseDisjoint (f i)) :
((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i) := fun _ hI _ hJ hIJ =>
disjoint_left.2 fun a haI haJ =>
hIJ <| funext fun i => (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)
