English
For a binary function f: α → β → γ with injectivity on f a for a ∈ s, the family { f a '' t } is pairwise disjoint iff the induced map (p ↦ f p.1 p.2) on s ×ˢ t is injective.
Русский
Для бинарной функции f: α → β → γ, для которых для каждого a ∈ s отображение f a является инъекцией, множество { f a } над t попарно непересекается тогда и только тогда, когда отображение p ↦ f p.1 p.2 на s × t инъективно.
LaTeX
$$$$\big( \forall a \in s, Injective (\lambda b, f a b) \big) \Rightarrow (s.PAIRWISE_DISJOINT (\lambda a, f a '' t) \iff (s \timesˢ t).InjOn (\lambda p, f p.1 p.2)).$$$$
Lean4
/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
disjoint iff `f` is injective . -/
theorem pairwiseDisjoint_image_right_iff {f : α → β → γ} {s : Set α} {t : Set β} (hf : ∀ a ∈ s, Injective (f a)) :
(s.PairwiseDisjoint fun a => f a '' t) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2 :=
by
refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
· suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
rw [h]
exact mem_image_of_mem _ hy.2
· refine disjoint_iff_inf_le.mpr ?_
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)
