English
If s and t are disjoint and p holds on all their elements, and f maps p-elements injectively to β, then s.pmap f hs and t.pmap f ht are disjoint.
Русский
Если s и t непересекаются и для всех элементов выполняется p, а отображение f переводит p-элементы в β инъективно, то s.pmap f hs и t.pmap f ht расходятся.
LaTeX
$$$ \\text{Disjoint } s t\\ ,\\ hs:\\forall a\\in s\\ p a,\\ ht:\\forall a\\in t\\ p a,\\ hf:\\forall a a', p a \\land p a' \\to f a\\ ha = f a' ha' \\to a=a' \\Rightarrow \\text{Disjoint } (s.\\text{pmap} f hs) (t.\\text{pmap} f ht) $$$
Lean4
/-- The images of disjoint lists under a partially defined map are disjoint -/
theorem disjoint_pmap {p : α → Prop} {f : ∀ a : α, p a → β} {s t : List α} (hs : ∀ a ∈ s, p a) (ht : ∀ a ∈ t, p a)
(hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') (h : Disjoint s t) :
Disjoint (s.pmap f hs) (t.pmap f ht) := by
simp only [Disjoint, mem_pmap]
rintro b ⟨a, ha, rfl⟩ ⟨a', ha', ha''⟩
apply h ha
rwa [hf a a' (hs a ha) (ht a' ha') ha''.symm]
