English
Equality of cardinalities #(s ⊻ t) = #s · #t is equivalent to injectivity of the map (a, b) ↦ a ⊔ b on s × t.
Русский
Равенство кардиналностей #(s ⊻ t) = #s · #t эквивалентно инъективности отображения (a, b) ↦ a ⊔ b на s × t.
LaTeX
$$$ #(s \\oplus t) = #s \\cdot #t \\iff (s \\timesˢ t : Set (\\alpha \\times \\alpha)).InjOn \\big( \\lambda x \\mapsto x.1 \\lor x.2 \\big) $$$
Lean4
theorem card_sups_iff : #(s ⊻ t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun x => x.1 ⊔ x.2 :=
card_image₂_iff