exists_span_set_card_eq_spanRank — Mathlib

English

There exists a generating set s with card(s) = spanRank(p) and span R s = p.

Русский

Существует порождающее множество s такое, что card(s) = spanRank(p) и span R s = p.

LaTeX

$$$\exists s : Set M, \#s = p.spanRank \land span R s = p$$$

Lean4

/-- Constructs a generating set with cardinality equal to the `spanRank` of the submodule -/
theorem exists_span_set_card_eq_spanRank (p : Submodule R M) : ∃ s : Set M, #s = p.spanRank ∧ span R s = p :=
  by
  rw [spanRank]
  obtain ⟨s, hs⟩ :
    ⨅ (s : { s : Set M // span R s = p }), #s ∈ Set.range (fun (s : { s : Set M // span R s = p }) ↦ #s) :=
    csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
  exact ⟨s.1, ⟨hs, s.2⟩⟩

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