image2_congr' — Mathlib

English

A simplified special case: if f(a,b) = f'(a,b) for all a,b, then image2 f s t = image2 f' s t.

Русский

Упрощённый частный случай: если для всех a,b выполняется f(a,b) = f'(a,b), то image2 f s t = image2 f' s t.

LaTeX

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

Lean4

/-- A common special case of `image2_congr` -/
theorem image2_congr' (h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s t :=
  image2_congr fun a _ b _ => h a b

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