English
For any s subset of α×β, s ∈ f × g iff there exists t ∈ f with, eventually in g, and for all x ∈ t, (x,y) ∈ s for all y.
Русский
Для любого множества s⊆α×β верно: s ∈ f × g тогда и только тогда, когда существует t ∈ f, такая что почти во всех y в g, и для всех x ∈ t, (x,y) ∈ s.
LaTeX
$$$\forall \{s \subseteq (\alpha \times \beta)\},\ s \in f \times g \iff \exists t \in f,\ \forall^\mathrm{f}\ y \in g,\ \forall x \in t,\ (x,y) \in s$$$
Lean4
theorem mem_prod_iff_left {s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ y in g, ∀ x ∈ t, (x, y) ∈ s :=
by
simp only [mem_prod_iff, prod_subset_iff]
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
exact exists_congr fun _ => Iff.rfl.and forall₂_swap
