map_neg₂ — Mathlib

English

If f is a bounded bilinear map, then the flipped map exchanging arguments is also a bounded bilinear map.

Русский

Если f — ограниченное билинейное отображение, то отражённое отображение, меняющее аргументы местами, тоже ограничено билинейно.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \rightarrow IsBoundedBilinearMap 𝕜 (\lambda p \mapsto f(p.2, p.1))$$$

Lean4

theorem map_neg₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (y : F) : f (-x) y = -f x y := by rw [f.map_neg, neg_apply]

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