card_diffs_iff — Mathlib

English

The equality |s \\ t| = |s| · |t| holds iff the map (a,b) ↦ a \\ b is injective on s × t.

Русский

Равенство кардинальности достигается тогда и только тогда, когда отображение (a,b) ↦ a \\ b на s × t инъективно.

LaTeX

$$$ |s \\\\ t| = |s| \\cdot |t| \\iff (s \\times t : Set (\\alpha \\times \\alpha)).InjOn (\\lambda x \\to x.1 \\setminus x.2) $$$

Lean4

theorem card_diffs_iff : #(s \\ t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun x ↦ x.1 \ x.2 :=
  card_image₂_iff

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