map₂_flip — Mathlib

English

If you flip the arguments of map₂ using the flipped bilinear map, you get the same result: map₂ f.flip q p = map₂ f p q.

Русский

При перестановке аргументов bilinear отображение остаётся тем же: map₂ f.flip q p = map₂ f p q.

LaTeX

$$map₂ f.flip q p = map₂ f p q$$

Lean4

theorem map₂_flip (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : map₂ f.flip q p = map₂ f p q :=
  by
  rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]
  rfl

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