flip_separatingRight — Mathlib

English

For a bilinear map B, the map obtained by swapping arguments (the flip) is right-separating if and only if the original map is left-separating.

Русский

Для билинейной формы B отображение с обменом аргументов (flip) является правоподлежащим разделяющим тогда и только тогда, когда исходная форма является левополосно разделяющей.

LaTeX

$$$B.flip.SeparatingRight \\leftrightarrow B.SeparatingLeft$$$

Lean4

@[simp]
theorem flip_separatingRight {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} : B.flip.SeparatingRight ↔ B.SeparatingLeft :=
  ⟨fun hB x hy ↦ hB x hy, fun hB x hy ↦ hB x hy⟩

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