image₂_congr — Mathlib

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

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