map_perm_map_iff — Mathlib

English

If for every a in l we have f a ~ g a, then the flatMap of f over l is permutation-equivalent to the flatMap of g over l.

Русский

Если для каждого элемента a списка l выполняется f a ~ g a, то l.flatMap f ~ l.flatMap g.

LaTeX

$$$\forall l:\ List\;\alpha,\; \forall \{f,g:\alpha\to List\beta\},\; (\forall a\in l,\; f a ~ g a) \rightarrow l.flatMap f ~ l.flatMap g$$$

Lean4

theorem map_perm_map_iff {l' : List α} {f : α → β} (hf : f.Injective) : map f l ~ map f l' ↔ l ~ l' :=
  calc
    map f l ~ map f l' ↔ Relation.Comp (· = map f ·) (· ~ ·) (map f l) l' := by rw [eq_map_comp_perm]
    _ ↔ l ~ l' := by simp [Relation.Comp, map_inj_right hf]

Похожие утверждения