English
For any family s: ι → Set α and S ⊆ ι, the family piiUnionInter(λ i, {s(i)}) S consists precisely of those sets that can be written as ⋂ i ∈ t s(i) for some finite t ⊆ S.
Русский
Для любой семье s: ι → Set α и подмножества S ⊆ ι множество piiUnionInter(λ i, {s(i)}) S состоит точно из множеств вида ⋂ i ∈ t s(i), для некоторого конечного t ⊆ S.
LaTeX
$$$\ piiUnionInter(\lambda i, \{s(i)\}) S = \{ s' \subseteq α \mid ∃ t : Finset\ ι, (↑t ⊆ S) ∧ s' = ⋂ i ∈ t, s(i) \}$$$
Lean4
theorem piiUnionInter_singleton_left (s : ι → Set α) (S : Set ι) :
piiUnionInter (fun i => ({s i} : Set (Set α))) S =
{s' : Set α | ∃ (t : Finset ι) (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i} :=
by
ext1 s'
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]
refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
grind
