dualMap_bijective_iff — Mathlib

English

Two linear maps f and f.dualMap are bijective simultaneously: f is bijective if and only if f.dualMap is bijective.

Русский

Дуальные отображения двух линейных отображений биективны одновременно: биективно ли отображение f тогда и только тогда, когда биективно его дуальное отображение.

LaTeX

$$$\\text{Bijective}(f^{\\ast}) \\iff \\text{Bijective}(f)$$$

Lean4

/-- `f.dualMap` is bijective if and only if `f` is -/
@[simp]
theorem dualMap_bijective_iff {f : V₁ →ₗ[K] V₂} : Function.Bijective f.dualMap ↔ Function.Bijective f := by
  simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]

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