card_pos_of_affineSpan_eq_top — Mathlib

English

If the affine span of the range of p is top, then the index type ι is nonempty (cardinality positive).

Русский

Если аффинная оболочка образа p равна верхнему, то множество индексов ι не пусто.

LaTeX

$$affineSpan k (Set.range p) = ⊤ → 0 < Fintype.card ι$$

Lean4

theorem card_pos_of_affineSpan_eq_top {ι : Type*} [Fintype ι] {p : ι → P} (h : affineSpan k (range p) = ⊤) :
    0 < Fintype.card ι := by
  obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h
  exact
    Fintype.card_pos_iff.mpr
      ⟨i⟩
        -- An instance with better keys for the context

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