English
If i ∈ S, then every set in π i is contained in piiUnionInter π S. This makes intuitive sense: the construction with a singleton index i includes at least the i-th family.
Русский
Если i ∈ S, то каждый элемент π i содержится в piiUnionInter π S.
LaTeX
$$$\text{If } hiS: i \in S,\ \pi i \subseteq piiUnionInter(\pi,S).$$$
Lean4
theorem subset_piiUnionInter {π : ι → Set (Set α)} {S : Set ι} {i : ι} (his : i ∈ S) : π i ⊆ piiUnionInter π S :=
by
have h_ss : { i } ⊆ S := by
intro j hj
rw [mem_singleton_iff] at hj
rwa [hj]
refine Subset.trans ?_ (piiUnionInter_mono_right h_ss)
rw [piiUnionInter_singleton]
exact subset_union_left