coe_basisOfPiSpaceOfLinearIndependent

English

Let ι be finite and hb : LinearIndependent K b for b : ι → (ι → K). Then the basisOfPiSpaceOfLinearIndependent hb, viewed as a function, equals b.

Русский

Пусть ι конечен и hb : линейно независимо векторное семейство b : ι → (ι → K). Тогда база basisOfPiSpaceOfLinearIndependent hb, как функция, совпадает с b.

LaTeX

$$$\\bigl(\\text{basisOfPiSpaceOfLinearIndependent hb}\\bigr) = b$ (как отображение $ι \\to (ι \\to K)$).$$

Lean4

@[simp]
theorem coe_basisOfPiSpaceOfLinearIndependent {ι : Type*} [Fintype ι] {b : ι → (ι → K)} (hb : LinearIndependent K b) :
    ⇑(basisOfPiSpaceOfLinearIndependent hb) = b :=
  by
  by_cases hι : Nonempty ι
  · simp [hι, basisOfPiSpaceOfLinearIndependent]
  · rw [basisOfPiSpaceOfLinearIndependent, dif_neg hι]
    ext i
    exact ((not_nonempty_iff.mp hι).false i).elim

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