mem_prod_iff_right — Mathlib

English

For any s ⊆ α×β, s ∈ f × g iff there exists t ∈ g with, eventually in f, and for all y ∈ t, (x,y) ∈ s for all x.

Русский

Для любого s⊆α×β верно: s ∈ f × g тогда и только тогда, существует t ∈ g such that почти во всех x в f, и для всех y ∈ t, (x,y) ∈ s.

LaTeX

$$$\forall \{s \subseteq (\alpha \times \beta)\},\ s \in f \times g \iff \exists t \in g,\ \forall^\mathrm{f}\ x \in f,\ \forall y \in t,\ (x,y) \in s$$$

Lean4

theorem mem_prod_iff_right {s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ x in f, ∀ y ∈ t, (x, y) ∈ s := by
  rw [prod_comm, mem_map, mem_prod_iff_left]; rfl

Похожие утверждения