flip_separatingLeft — Mathlib

English

The left-separating property of a bilinear form is equivalent to the right-separating property of its flip.

Русский

Левополосное разделяющее свойство билинейной формы эквивалентно правополосному разделяющему свойству её перевёрнутой формы.

LaTeX

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

Lean4

@[simp]
theorem flip_separatingLeft {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} : B.flip.SeparatingLeft ↔ SeparatingRight B := by
  rw [← flip_separatingRight, flip_flip]

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