English
The cast of the cardinality of the intersection equals the cardinalities combined minus the intersection cardinality, in an additive group with one.
Русский
Сумма кардиналностей пересечения и объединения минус пересечение, приведённая в группу с единицей.
LaTeX
$$$\\operatorname{card}(s \\cap t)^{R} = (\\operatorname{card}(s) + \\operatorname{card}(t) - \\operatorname{card}(s \\cup t))$$$
Lean4
theorem cast_card_inter : (#(s ∩ t) : R) = #s + #t - #(s ∪ t) := by
rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]