English
If for every b in t the map a ↦ f a b is injective, then the family { (f a b) } over a ∈ s, b ∈ t is pairwise disjoint iff the map (p ↦ f p.1 p.2) on s ×ˢ t is injective.
Русский
Если для каждого b ∈ t отображение a ↦ f a b инъективно, тогда семейство { f a b } по a ∈ s, b ∈ t попарно непересекается тогда и только тогда, когда отображение (p.fst, p.snd) ↦ f p.fst p.snd инъективно.
LaTeX
$$$$\big( \forall b \in t, Injective (\lambda a, f a b) \big) \Rightarrow (t.PAIRWISE_DISJOINT (\lambda b, (\lambda a, f a b) '' s) \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_left_iff {f : α → β → γ} {s : Set α} {t : Set β}
(hf : ∀ b ∈ t, Injective fun a => f a b) :
(t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2 :=
by
refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩
· suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)
rw [h]
exact mem_image_of_mem _ hy.1
· refine disjoint_iff_inf_le.mpr ?_
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)
