symm — Mathlib

English

The map f(-x, y) = -f(x,y) for a bilinear map.

Русский

Отображение f(-x,y) = -f(x,y) для билинейного отображения.

LaTeX

$$$f(-x,y) = -f(x,y)$$$

Lean4

theorem symm (h : IsBoundedBilinearMap 𝕜 f) : IsBoundedBilinearMap 𝕜 (fun p ↦ f (p.2, p.1))
    where
  add_left x₁ x₂ y := h.add_right _ _ _
  smul_left c x y := h.smul_right _ _ _
  add_right x y₁ y₂ := h.add_left _ _ _
  smul_right c x y := h.smul_left _ _ _
  bound := by
    obtain ⟨C, hC_pos, hC⟩ := h.bound
    exact ⟨C, hC_pos, fun x y ↦ (hC y x).trans_eq (by ring)⟩

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