English
Let f: α→β, g: β→γ be filters and s ⊆ γ. Then s ∈ (f.map m).seq g iff ∃ t ∈ g, ∃ u ∈ f such that ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s.
Русский
Пусть f: α→β, g: β→γ — фильтры и s ⊆ γ. Тогда s ∈ (f.map m).seq g эквивалентно существованию t ∈ g и u ∈ f такие, что ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s.
LaTeX
$$$ s \in (f.map m).seq g \iff \exists t \in g, \exists u \in f, \forall x \in u, \forall y \in t, m\,x\,y \in s $$$
Lean4
theorem mem_map_seq_iff {f : Filter α} {g : Filter β} {m : α → β → γ} {s : Set γ} :
s ∈ (f.map m).seq g ↔ ∃ t u, t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s :=
Iff.intro (fun ⟨t, ht, s, hs, hts⟩ => ⟨s, m ⁻¹' t, hs, ht, fun _ => hts _⟩) fun ⟨t, s, ht, hs, hts⟩ =>
⟨m '' s, image_mem_map hs, t, ht, fun _ ⟨_, has, Eq⟩ => Eq ▸ hts _ has⟩
