card_toLeft_add_card_toRight — Mathlib

English

Let u be a finite set of elements from α ⊕ β. Denote by u^{toLeft} and u^{toRight} its projections onto α and β, respectively. Then the total number of elements of u equals the sum of the numbers of elements in its left and right projections: |u^{toLeft}| + |u^{toRight}| = |u|.

Русский

Пусть u — конечное множество из элементов α ⊕ β. Обозначим через u^{toLeft} и u^{toRight} соответствующие проекции на α и β. Тогда сумма кардинальностей левой и правой частей равна кардинальности u: |u^{toLeft}| + |u^{toRight}| = |u|.

LaTeX

$$$|u^{\mathrm{toLeft}}| + |u^{\mathrm{toRight}}| = |u|$$$

Lean4

theorem card_toLeft_add_card_toRight : #u.toLeft + #u.toRight = #u := by rw [← card_disjSum, toLeft_disjSum_toRight]

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