English
Let f be a filter on α, g a filter on β, h a filter on γ, and m: α × β → γ. Then h is below map₂ m f g if and only if for every set s in f and every set t in g, the two-variable image image2 m s t belongs to h.
Русский
Пусть f — фильтр на α, g — фильтр на β, h — фильтр на γ, и m: α × β → γ. Тогда h ≤ map₂ m f g тогда и только тогда, когда для всякого множества s ∈ f и каждого t ∈ g выполняется, что image2 m s t ∈ h.
LaTeX
$$$ h \le map_2 m f g \iff \forall s \in f, \forall t \in g, image2\ m\ s\ t \in h $$$
Lean4
@[simp]
theorem le_map₂_iff {h : Filter γ} : h ≤ map₂ m f g ↔ ∀ ⦃s⦄, s ∈ f → ∀ ⦃t⦄, t ∈ g → image2 m s t ∈ h :=
⟨fun H _ hs _ ht => H <| image2_mem_map₂ hs ht, fun H _ ⟨_, hs, _, ht, hu⟩ => mem_of_superset (H hs ht) hu⟩
