linearIndependentSingleton — Mathlib

English

The evaluation on a singleton false is linearly independent.

Русский

Оценка на единичном {false} линейно независима.

LaTeX

$$$$\\text{LinearIndependent}\\; \\mathbb{Z}\\; \\big( \\mathrm{GoodProducts}.\\mathrm{eval} (\\mathrm{Set.instSingletonSet}.singleton (\\mathrm{Bool.false})) \\big)$$$$

Lean4

theorem linearIndependentSingleton {I} [LinearOrder I] :
    LinearIndependent ℤ (eval ({fun _ ↦ false} : Set (I → Bool))) :=
  by
  refine linearIndependent_unique (eval ({fun _ ↦ false} : Set (I → Bool))) ?_
  simp [eval, Products.eval, Products.nil, default]

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