English
For any s ⊆ α×β, la, lb filters, membership of the complement s^c in la.coprod lb is equivalent to the membership of the complements of the projections in la and lb respectively.
Русский
Для множества s ⊆ α×β верно: s^c принадлежит la.coprod lb тогда и только тогда, когда прообразы по fst и по snd комплементов s принадлежат la и lb соответственно.
LaTeX
$$$ s^{c} \in l.coprod m \iff (\mathrm{Prod.fst} \ '' s)^{c} \in l \land (\mathrm{Prod.snd} \ '' s)^{c} \in m $$$
Lean4
theorem compl_mem_coprod {s : Set (α × β)} {la : Filter α} {lb : Filter β} :
sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb := by
simp only [Filter.coprod, mem_sup, compl_mem_comap]
