funCongrLeft_apply — Mathlib

English

The application of the congrLeft construction to an equivalence e and a map x equals applying the corresponding funLeft to x.

Русский

Применение конглев слева к эквивелентности e и отображению x равно применению соответствующего funLeft к x.

LaTeX

$$$ (\mathrm{funCongrLeft}\; R\; M\; e)\; x = (\mathrm{funLeft}\; R\; M\; e)\; x $$$

Lean4

@[simp]
theorem funCongrLeft_apply (e : m ≃ n) (x : n → M) : funCongrLeft R M e x = funLeft R M e x :=
  rfl

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