mem_image₂ — Mathlib

English

The image of a binary function f under Finset is defined by applying f to all pairs from s × t via uncurry.

Русский

Образ бинарной функции f в Finset определяется как применение f ко всем парам из s × t через uncurry.

LaTeX

$$image₂ f s t := (s ×ˢ t).image (uncurry f)$$

Lean4

@[simp]
theorem mem_image₂ : c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c := by simp [image₂, and_assoc]

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