mem_image2 — Mathlib

English

c belongs to the image2 of f on s and t iff there exist a ∈ s and b ∈ t with f(a,b) = c.

Русский

Элемент c принадлежит image2 f s t тогда и только тогда, когда существуют a ∈ s и b ∈ t такие, что f(a,b) = c.

LaTeX

$$$$ c \\in \\operatorname{image2}(f,s,t) \\iff \\exists a \\in s, \\exists b \\in t, f(a,b) = c $$$$

Lean4

@[simp, grind =]
theorem mem_image2 : c ∈ image2 f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c :=
  .rfl

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