nontrivial_dual_iff — Mathlib

English

The dual is nontrivial iff the original space is nontrivial.

Русский

Дуал не тривиален тогда и только тогда, когда исходное пространство не тривиально.

LaTeX

$$Nontrivial($V^{\\ast}$) $\\iff$ Nontrivial($V$)$$

Lean4

@[simp]
theorem nontrivial_dual_iff : Nontrivial (Dual K V) ↔ Nontrivial V := by
  rw [← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton, subsingleton_dual_iff]

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