prodCongr_apply — Mathlib

English

The action of prodCongr on an element x ∈ S × T coincides with the standard product-congruence applied to x; i.e., (l.prodCongr r) x = Equiv.prodCongr l r x.

Русский

Действие prodCongr на элемент x ∈ S × T совпадает с обычной конгруэнцией произведения: (l.prodCongr r) x = Equiv.prodCongr l r x.

LaTeX

$$$$ \\forall x, \\ (l.prodCongr r) x = Equiv.prodCongr l r x. $$$$

Lean4

@[simp low]
theorem prodCongr_apply (x : S × T) : prodCongr l r x = Equiv.prodCongr l r x :=
  rfl

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