prod_subset_iff — Mathlib

English

Let s ⊆ α, t ⊆ β, and P ⊆ α × β. Then s × t ⊆ P if and only if for every x ∈ s and every y ∈ t, (x, y) ∈ P.

Русский

Пусть s ⊆ α, t ⊆ β, P ⊆ α × β. Тогда s × t ⊆ P тогда и только тогда, когда для каждого x ∈ s и каждого y ∈ t, (x, y) ∈ P.

LaTeX

$$$ s \times t \subseteq P \iff \forall x \in s, \forall y \in t, (x,y) \in P $$$

Lean4

theorem prod_subset_iff {P : Set (α × β)} : s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P :=
  ⟨fun h _ hx _ hy => h (mk_mem_prod hx hy), fun h ⟨_, _⟩ hp => h _ hp.1 _ hp.2⟩

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