English
For s ⊆ α×β, s ∈ f ×ˢ g iff there exist t1 ∈ f and t2 ∈ g with t1 ×ˢ t2 ⊆ s.
Русский
Для множества s ⊆ α×β верно: s ∈ f ×ˢ g тогда и только тогда, когда существуют t1 ∈ f и t2 ∈ g такие, что t1 × t2 ⊆ s.
LaTeX
$$$s \\in f \\timesˢ g \\iff \\exists t_1 \\in f, \\exists t_2 \\in g, t_1 \\timesˢ t_2 \\subseteq s$$$
Lean4
theorem mem_prod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} : s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s :=
by
constructor
· rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
· rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h
