image2_congr — Mathlib

English

If f and f' agree on all a ∈ s and b ∈ t, then image2 f s t = image2 f' s t.

Русский

Если для всех a ∈ s и b ∈ t выполняется f(a,b) = f'(a,b), то image2 f s t = image2 f' s t.

LaTeX

$$$$ \\Bigl(\\forall a \\in S, \\forall b \\in T,\; f(a,b) = f'(a,b)\\Bigr) \\Rightarrow \\operatorname{image2} f S T = \\operatorname{image2} f' S T. $$$$

Lean4

@[congr]
theorem image2_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image2 f s t = image2 f' s t := by grind

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