English
For any f, join distributes over map: 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) : Seq.map f (Seq.join S) = Seq.join (Seq.map (map f) S) :=
by
apply
Seq.eq_of_bisim fun s1 s2 =>
∃ s S, s1 = Seq.append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
· intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, S, rfl, rfl⟩ => by
cases s <;> simp
case nil =>
cases S <;> simp
case cons x S =>
obtain ⟨a, s⟩ := x
simpa [map] using ⟨_, _, rfl, rfl⟩
case cons _ s => exact ⟨s, S, rfl, rfl⟩
· refine ⟨nil, S, ?_, ?_⟩ <;> simp
