English
There is a relator compatibility for flatMap with a swap, i.e., relating flatMaps through a transformed relation and flattening.
Русский
Существуют совместимости релятора для flatMap через транспонированное отношение и уплощение.
LaTeX
$$$ \mathrm{rel\_flatMap} : (\mathrm{Forall₂}\ R \Rightarrow (R \Rightarrow \mathrm{Forall₂ P}) \Rightarrow \mathrm{Forall₂ P})\ (\mathrm{Function.swap}\ \mathrm List.flatMap)\ (\mathrm{Function.swap}\ List.flatMap)$$$
Lean4
theorem rel_flatMap :
(Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) (Function.swap List.flatMap) (Function.swap List.flatMap) :=
fun _ _ h₁ _ _ h₂ => rel_flatten (rel_map (@h₂) h₁)
