English
For a relation-preserving map f, destutter commutes with map: map f (destutter R l) = destutter R₂ (map f l) whenever R a b ↔ R₂ (f a) (f b) for all a,b in l.
Русский
При отображении, сохраняющем отношение, destutter и map взаимно приводят к одному результату: map f (destutter R l) = destutter R₂ (map f l) при условии, что R а b эквивалентно R₂ (f a) (f b) для всех a,b из l.
LaTeX
$$$$\text{map}_{f}(\operatorname{destutter} R l) = \operatorname{destutter} R_{2}(\text{map}_{f} l)$$$$
Lean4
/-- For a relation-preserving map, `destutter` commutes with `map`. -/
theorem map_destutter {f : α → β} :
∀ {l : List α}, (∀ a ∈ l, ∀ b ∈ l, R a b ↔ R₂ (f a) (f b)) → (l.destutter R).map f = (l.map f).destutter R₂
| [], hl => by simp
| [a], hl => by simp
| a :: b :: l, hl => by
have := hl a (by simp) b (by simp)
simp_rw [map_cons, destutter_cons_cons, ← this]
by_cases hr : R a b <;>
simp [hr, ← destutter_cons',
map_destutter fun c hc d hd ↦
hl _ (cons_subset_cons _ (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]
