Theorems · Theorem · general topology

Filter.mem_map_seq_iff

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {m : α → β → γ} {s : Set γ},
  s ∈ (Filter.map m f).seq g ↔ ∃ t u, t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s

Defined in

Mathlib.Order.Filter.Map

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms