English
For a function f : α → β → γ, sets s ⊆ α and t ⊆ β, and a ∈ α, b ∈ β, under suitable injectivity conditions, image2 f s t is infinite iff either s is infinite and t is nonempty or t is infinite and s is nonempty.
Русский
Для функции f : α → β → γ и множеств S ⊆ α, T ⊆ β, образ image2 f S T бесконечен тогда и только тогда, когда либо S бесконечно и T непусто, либо T бесконечно и S непусто.
LaTeX
$$$ \forall f \; s \; t,\ (\forall b \in t, InjOn (fun a => f a b) s) \to (\forall a \in s, InjOn (f a) t) \Rightarrow (image2 f s t).Infinite \iff (s.Infinite \land t.Nonempty) \lor (t.Infinite \land s.Nonempty) $$$
Lean4
theorem infinite_image2 (hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
(image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty :=
by
refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
· rw [← image_uncurry_prod] at h
exact h.of_image _
· rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
· exact hs.image2_left hb (hfs _ hb)
· exact ht.image2_right ha (hft _ ha)
