English
If f and f' agree pointwise on s × t, then image₂ f s t = image₂ f' s t.
Русский
Если для всех a∈s и b∈t имеют f a b = f' a b, то image₂ f s t = image₂ f' s t.
LaTeX
$$$\\forall a \\in s, \\\\forall b \\in t, f a b = f' a b \\Rightarrow \\operatorname{image}_2 f s t = \\operatorname{image}_2 f' s t$$$
Lean4
theorem image₂_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image₂ f s t = image₂ f' s t :=
coe_injective <| by
push_cast
exact image2_congr h