card_toRight_le — Mathlib

English

Similarly, for any finite set u of α ⊕ β, the right projection is no larger than u: |u^{toRight}| ≤ |u|.

Русский

Аналогично, для любого конечного множества u над α ⊕ β правая проекция не превосходит само множество: |u^{toRight}| ≤ |u|.

LaTeX

$$|u^{\mathrm{toRight}}| \le |u|$$

Lean4

theorem card_toRight_le : #u.toRight ≤ #u :=
  (Nat.le_add_left _ _).trans_eq card_toLeft_add_card_toRight

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