le_of_fin_surjective — Mathlib

English

If f: (Fin n → R) →ₗ Fin m → R is surjective under RankCondition R, then m ≤ n.

Русский

Если f: (Fin n → R) →ₗ Fin m → R сюръективно, то m ≤ n.

LaTeX

$$$\text{If } f:\mathrm{Fin}(n) \to R \to_\mathrm{lin} \mathrm{Fin}(m) \to R \text{ is surjective, then } m \le n.$$$

Lean4

theorem le_of_fin_surjective [RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R) : Surjective f → m ≤ n :=
  RankCondition.le_of_fin_surjective f

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