mem_map₂_iff — Mathlib

English

For every c, c belongs to map₂ f a b if and only if there exist a' ∈ a and b' ∈ b with f a' b' = c.

Русский

Для каждого c верно: c ∈ map₂ f a b тогда и только тогда, когда существуют a' ∈ a и b' ∈ b такие, что f a' b' = c.

LaTeX

$$$ c \in \mathrm{map}_2 f\ a\ b \iff \exists a'\in a\,\exists b'\in b,\ f\ a'\ b' = c $$$

Lean4

theorem mem_map₂_iff {c : γ} : c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c := by grind

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