card_sups_iff — Mathlib

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

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