exists_le_ker_of_lt_top — Mathlib

English

Let p be a proper subspace of V. Then there exists a nonzero linear functional f: V → K with p ⊆ ker f.

Русский

Пусть p является ненормальным (правным) подпространством V. Тогда существует ненулевой линейный функционал f: V → K, такой что p ⊆ ker f.

LaTeX

$$$p < \top \;\Rightarrow\; \exists f: V \to_K K,\; f \neq 0 \wedge p \le \ker f$$$

Lean4

/-- If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map
`f : V →ₗ[K] K` such that `p ≤ ker f`. -/
theorem exists_le_ker_of_lt_top (p : Submodule K V) (hp : p < ⊤) : ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ ker f :=
  by
  rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩
  rcases exists_le_ker_of_notMem hpv with ⟨f, hfv, hpf⟩
  exact ⟨f, ne_of_apply_ne (· v) hfv, hpf⟩

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