flip_injective_iff₁ — Mathlib

English

For a bilinear map B, the injectivity of B.flip is equivalent to the surjectivity of B, under finite dimensionality assumptions.

Русский

Для билинейного отображения B инъективность B.flip эквивалентна сюръективности B при конечном размерности.

LaTeX

$$$\\text{Injective}(B^{\\mathrm{flip}}) \\iff \\text{Surjective}(B)$$$

Lean4

theorem flip_injective_iff₁ [FiniteDimensional K V₁] : Injective B.flip ↔ Surjective B := by
  rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]; rfl

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