subsingleton_dual_iff — Mathlib

English

The dual is subsingleton iff the original space is subsingleton.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem subsingleton_dual_iff : Subsingleton (Dual K V) ↔ Subsingleton V :=
  ⟨fun _ ↦ ⟨fun _ _ ↦ eval_apply_injective K (Subsingleton.elim ..)⟩, fun _ ↦ inferInstance⟩

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