eq_top_iff_forall_basis_mem — Mathlib

English

A submodule p equals the top submodule if and only if every basis vector lies in p.

Русский

Подмодуль p равен верхнему тогда и только тогда, когда каждый вектор базиса принадлежит p.

LaTeX

$$$p = \top \iff \forall i, b_i \in p$.$$

Lean4

theorem _root_.Submodule.eq_top_iff_forall_basis_mem {p : Submodule R M} : p = ⊤ ↔ ∀ i, b i ∈ p :=
  by
  refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
  replace h : range b ⊆ p := by rintro - ⟨i, rfl⟩; exact h i
  simpa using span_mono (R := R) h

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