exists_affineBasis_of_finiteDimensional

English

If ι is finite, V is finite-dimensional, and the dimension relation holds, then there exists an affine basis of ι k P.

Русский

Если ι конечно, V конечноразмерно над k и выполняется размерность, существует аффинная база индексированная ι.

LaTeX

$$Nonempty (AffineBasis ι k P)$$

Lean4

theorem exists_affineBasis_of_finiteDimensional [Fintype ι] [FiniteDimensional k V]
    (h : Fintype.card ι = Module.finrank k V + 1) : Nonempty (AffineBasis ι k P) :=
  by
  obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P
  lift s to Finset P using b.finite_set
  refine ⟨b.reindex <| Fintype.equivOfCardEq ?_⟩
  rw [h, ← b.card_eq_finrank_add_one]

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