map₂_eq_some_iff — Mathlib

English

The equation map₂ f a b = some c holds iff there exist a' ∈ a and b' ∈ b with f a' b' = c.

Русский

Уравнение map₂ f a b = some c имеет решение тогда и только тогда, когда существуют a' ∈ a и b' ∈ b с f a' b' = c.

LaTeX

$$$ map_2 f\ a\ b = \mathrm{some}\ c \iff \exists a'\in a\;\exists b'\in b\;\ f\ a' b' = c $$$

Lean4

/-- `simp`-normal form of `mem_map₂_iff`. -/
@[simp]
theorem map₂_eq_some_iff {c : γ} : map₂ f a b = some c ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c := by grind

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