English
The associativity of seq holds: seq h (seq g x) = seq (seq (map (· ∘ ·) h) g) x.
Русский
Свойство ассоциативности последовательностей: seq h (seq g x) = seq (seq (map (· ∘ ·) h) g) x.
LaTeX
$$$ \operatorname{seq} h (\operatorname{seq} g x) = \operatorname{seq} (\operatorname{seq} (\operatorname{map} (\cdot \circ \cdot) h) g) x $$$
Lean4
@[simp]
theorem seq_assoc (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)) :
seq h (seq g x) = seq (seq (map (· ∘ ·) h) g) x :=
by
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
· rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩
refine mem_of_superset ?_ (Set.seq_mono ((Set.seq_mono hu Subset.rfl).trans hs) Subset.rfl)
rw [← Set.seq_seq]
exact seq_mem_seq hw (seq_mem_seq hv ht)
· rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
refine mem_of_superset ?_ (Set.seq_mono Subset.rfl ht)
rw [Set.seq_seq]
exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv
