English
Given a filter f on functions α→β and a filter g on α, the applicative sequencing filter f ⊗ g (seq) is the filter on β consisting of sets S such that there exist U ∈ f and T ∈ g with ∀ m ∈ U, ∀ x ∈ T, m(x) ∈ S.
Русский
Пусть фильтр f на функций α→β и фильтр g на α. Аппликативное секвенирование означает фильтр на β, где S принадлежит этому фильтру, если существует U ∈ f и T ∈ g такие, что для всех m ∈ U и всех x ∈ T выполняется m(x) ∈ S.
LaTeX
$$$S \in \mathrm{seq}(f,g) \iff \exists U \in f, \exists T \in g, \forall m \in U, \forall x \in T, (m\,x) \in S.$$$
Lean4
/-- The applicative sequentiation operation. This is not induced by the bind operation. -/
def seq (f : Filter (α → β)) (g : Filter α) : Filter β
where
sets := {s | ∃ u ∈ f, ∃ t ∈ g, ∀ m ∈ u, ∀ x ∈ t, (m : α → β) x ∈ s}
univ_sets := ⟨univ, univ_mem, univ, univ_mem, fun _ _ _ _ => trivial⟩
sets_of_superset := fun ⟨t₀, t₁, h₀, h₁, h⟩ hst => ⟨t₀, t₁, h₀, h₁, fun _ hx _ hy => hst <| h _ hx _ hy⟩
inter_sets := fun ⟨t₀, ht₀, t₁, ht₁, ht⟩ ⟨u₀, hu₀, u₁, hu₁, hu⟩ =>
⟨t₀ ∩ u₀, inter_mem ht₀ hu₀, t₁ ∩ u₁, inter_mem ht₁ hu₁, fun _ ⟨hx₀, hx₁⟩ _ ⟨hy₀, hy₁⟩ =>
⟨ht _ hx₀ _ hy₀, hu _ hx₁ _ hy₁⟩⟩
