English
The equality |s ⊼ t| = |s| · |t| holds if and only if the map (a,b) ↦ a ⊓ b is injective on s × t.
Русский
Равенство кардиналов |s ⊼ t| = |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 => x.1 \sqcap x.2) $$$
Lean4
theorem card_infs_iff : #(s ⊼ t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun x => x.1 ⊓ x.2 :=
card_image₂_iff