exists_mem_ne_zero_of_ne_bot — Mathlib

English

Let p be a submodule of M with p ≠ ⊥. Then there exists a nonzero element b ∈ p.

Русский

Пусть p — подпространство пространства M над кольцом R и p ≠ ⊥. Тогда существует элемент b ≠ 0, такой что b ∈ p.

LaTeX

$$$\exists b \in M,\ b \in p \land b \neq 0$$$

Lean4

theorem exists_mem_ne_zero_of_ne_bot {p : Submodule R M} (h : p ≠ ⊥) : ∃ b : M, b ∈ p ∧ b ≠ 0 :=
  let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp h
  ⟨b, hb₁, hb₂⟩
    -- FIXME: we default PUnit to PUnit.{1} here without the explicit universe annotation

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