English
Mapping over a join distributes over the join: map f (join S) = join (map (map f) S).
Русский
Отображение по объединению распространяется на сочетание: map f (join S) = join (map (map f) S).
LaTeX
$$$$ \\operatorname{map} f (\\mathrm{join} S) = \\mathrm{join}(\\operatorname{map}(\\operatorname{map} f) S) $$$$
Lean4
@[simp]
theorem map_join (f : α → β) (S) : map f (join S) = join (map (map f) S) :=
by
apply Seq.eq_of_bisim fun s1 s2 => ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
· intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, S, rfl, rfl⟩ => by
induction s using WSeq.recOn <;> simp
· induction S using WSeq.recOn <;> simp
case cons s S => exact ⟨map f s, S, rfl, rfl⟩
case think S => refine ⟨nil, S, ?_, ?_⟩ <;> simp
· exact ⟨_, _, rfl, rfl⟩
· exact ⟨_, _, rfl, rfl⟩
· refine ⟨nil, S, ?_, ?_⟩ <;> simp
