English
Let R be a ring with RankCondition. If α,β are finite types and f : (α → R) →ₗ β → R is injective, then card α ≤ card β.
Русский
Пусть R удовлетворяет RankCondition. Пусть α, β конечные множества. Если f : (α → R) →ₗ β → R инъективна, тогда card(α) ≤ card(β).
LaTeX
$$$\text{Let } R\text{ satisfy RankCondition. If } f:(\alpha \to R) \to_\mathrm{lin} (\beta \to R)\text{ is injective, then } |\alpha| \le |\beta|.$$$
Lean4
theorem card_le_of_injective [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β] (f : (α → R) →ₗ[R] β → R)
(i : Injective f) : Fintype.card α ≤ Fintype.card β :=
by
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
exact
le_of_fin_injective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
(((LinearEquiv.symm Q).injective.comp i).comp (LinearEquiv.injective P))
