card_infs_iff — Mathlib

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

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