image₂_congr' — Mathlib

English

If two-argument function f and f' agree pointwise on the inputs, then their image₂ over fixed finite sets s and t are equal.

Русский

Если бинарные функции f и f' совпадают по каждому аргументу, то их image₂ на заданных конечных множествах s и t совпадает.

LaTeX

$$(∀ a b, f a b = f' a b) → Finset.image₂ f s t = Finset.image₂ f' s t$$

Lean4

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

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