English
Characterization of membership in a coprod: s ∈ f.coprod g iff there exist t1 ∈ f with fst⁻¹' t1 ⊆ s and t2 ∈ g with snd⁻¹' t2 ⊆ s.
Русский
Характеризация принадлежности элемента в копрод: s принадлежит f.coprod g тогда и только тогда, когда существуют t1 ∈ f и t2 ∈ g такие, что fst^-1'(t1) ⊆ s и snd^-1'(t2) ⊆ s.
LaTeX
$$$ s \\in f.coprod g \\iff (\\exists t_{1} \\in f, \\operatorname{Prod.fst}^{-1}' t_{1} \\subseteq s) \\land (\\exists t_{2} \\in g, \\operatorname{Prod.snd}^{-1}' t_{2} \\subseteq s) $$$
Lean4
theorem mem_coprod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s := by simp [Filter.coprod]
