card' — Mathlib

English

A variant form: |V| = |ℙ_k(V)|·(|k|−1) + 1 when V and k are finite.

Русский

Вариант формы: |V| = |ℙ_k(V)|·(|k|−1) + 1, когда V и k конечны.

LaTeX

$$$ |V| = |\mathbb{P}_k(V)| \cdot (|k| - 1) + 1 $$$

Lean4

/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite with less
natural subtraction. -/
theorem card' [Finite V] : Nat.card V = Nat.card (ℙ k V) * (Nat.card k - 1) + 1 :=
  by
  rw [← card k V]
  have : Nat.card V > 0 := Nat.card_pos
  cutsat

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