Theorems about map and comap on filters.

Push-forwards, pull-backs, and the monad structure

@[simp]

theorem Filter.map_principal {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : map f (principal s) = principal (f '' s)

@[simp]

theorem Filter.eventually_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop} : (∀ᶠ (b : β) in map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)

@[simp]

theorem Filter.frequently_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop} : (∃ᶠ (b : β) in map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)

@[simp]

theorem Filter.eventuallyEq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {f₁ f₂ : β → γ} : f₁ =ᶠ[map m f] f₂ ↔ f₁ ∘ m =ᶠ[f] f₂ ∘ m

@[simp]

theorem Filter.eventuallyLE_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} [LE γ] {f₁ f₂ : β → γ} : f₁ ≤ᶠ[map m f] f₂ ↔ f₁ ∘ m ≤ᶠ[f] f₂ ∘ m

@[simp]

theorem Filter.mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ map m f ↔ m ⁻¹' t ∈ f

theorem Filter.mem_map' {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ map m f ↔ {x : α | m x ∈ t} ∈ f

theorem Filter.image_mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α} (hs : s ∈ f) : m '' s ∈ map m f

@[simp]

theorem Filter.image_mem_map_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α} (hf : Function.Injective m) : m '' s ∈ map m f ↔ s ∈ f

theorem Filter.range_mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : Set.range m ∈ map m f

theorem Filter.mem_map_iff_exists_image {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ map m f ↔ ∃ s ∈ f, m '' s ⊆ t

@[simp]

theorem Filter.map_id {α : Type u_1} {f : Filter α} : map id f = f

@[simp]

theorem Filter.map_id' {α : Type u_1} {f : Filter α} : map (fun (x : α) => x) f = f

@[simp]

theorem Filter.map_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : α → β} {m' : β → γ} : map m' ∘ map m = map (m' ∘ m)

@[simp]

theorem Filter.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {m' : β → γ} : map m' (map m f) = map (m' ∘ m) f

theorem Filter.map_congr {α : Type u_1} {β : Type u_2} {m₁ m₂ : α → β} {f : Filter α} (h : m₁ =ᶠ[f] m₂) : map m₁ f = map m₂ f

If functions m₁ and m₂ are eventually equal at a filter f, then they map this filter to the same filter.

theorem Filter.mem_comap' {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} : s ∈ comap f l ↔ {y : β | ∀ ⦃x : α⦄, f x = y → x ∈ s} ∈ l

theorem Filter.mem_comap'' {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} : s ∈ comap f l ↔ Set.kernImage f s ∈ l

theorem Filter.mem_comap_prodMk {α : Type u_1} {β : Type u_2} {x : α} {s : Set β} {F : Filter (α × β)} : s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F

RHS form is used, e.g., in the definition of UniformSpace.

@[deprecated Filter.mem_comap_prodMk (since := "2025-03-10")]

theorem Filter.mem_comap_prod_mk {α : Type u_1} {β : Type u_2} {x : α} {s : Set β} {F : Filter (α × β)} : s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F

Alias of Filter.mem_comap_prodMk.

---

RHS form is used, e.g., in the definition of UniformSpace.

@[simp]

theorem Filter.eventually_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {p : α → Prop} : (∀ᶠ (a : α) in comap f l, p a) ↔ ∀ᶠ (b : β) in l, ∀ (a : α), f a = b → p a

@[simp]

theorem Filter.frequently_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {p : α → Prop} : (∃ᶠ (a : α) in comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ (a : α), f a = b ∧ p a

theorem Filter.mem_comap_iff_compl {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} : s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

theorem Filter.compl_mem_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} : sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

instance Filter.instLawfulFunctor : LawfulFunctor Filter

theorem Filter.pure_sets {α : Type u_1} (a : α) : (pure a).sets = {s : Set α | a ∈ s}

@[simp]

theorem Filter.eventually_pure {α : Type u_1} {a : α} {p : α → Prop} : (∀ᶠ (x : α) in pure a, p x) ↔ p a

@[simp]

theorem Filter.principal_singleton {α : Type u_1} (a : α) : principal {a} = pure a

@[simp]

theorem Filter.map_pure {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (pure a) = pure (f a)

theorem Filter.pure_le_principal {α : Type u_1} {s : Set α} (a : α) : pure a ≤ principal s ↔ a ∈ s

@[simp]

theorem Filter.join_pure {α : Type u_1} (f : Filter α) : (pure f).join = f

@[simp]

theorem Filter.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (m : α → Filter β) : (pure a).bind m = m a

theorem Filter.map_bind {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : β → γ) (f : Filter α) (g : α → Filter β) : map m (f.bind g) = f.bind (map m ∘ g)

theorem Filter.bind_map {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : α → β) (f : Filter α) (g : β → Filter γ) : (map m f).bind g = f.bind (g ∘ m)

Filter as a Monad

In this section we define Filter.monad, a Monad structure on Filters. This definition is not an instance because its Seq projection is not equal to the Filter.seq function we use in the Applicative instance on Filter.

def Filter.monad : Monad Filter

The monad structure on filters.

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.lawfulMonad : LawfulMonad Filter

instance Filter.instAlternative : Alternative Filter

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Filter.map_def {α β : Type u_6} (m : α → β) (f : Filter α) : m <$> f = map m f

@[simp]

theorem Filter.bind_def {α β : Type u_6} (f : Filter α) (m : α → Filter β) : f >>= m = f.bind m

map and comap equations

@[simp]

theorem Filter.mem_comap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {s : Set α} : s ∈ comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s

theorem Filter.preimage_mem_comap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {t : Set β} (ht : t ∈ g) : m ⁻¹' t ∈ comap m g

theorem Filter.Eventually.comap {α : Type u_1} {β : Type u_2} {g : Filter β} {p : β → Prop} (hf : ∀ᶠ (b : β) in g, p b) (f : α → β) : ∀ᶠ (a : α) in Filter.comap f g, p (f a)

theorem Filter.comap_id {α : Type u_1} {f : Filter α} : comap id f = f

theorem Filter.comap_id' {α : Type u_1} {f : Filter α} : comap (fun (x : α) => x) f = f

theorem Filter.comap_const_of_notMem {α : Type u_1} {β : Type u_2} {g : Filter β} {t : Set β} {x : β} (ht : t ∈ g) (hx : x ∉ t) : comap (fun (x_1 : α) => x) g = ⊥

@[deprecated Filter.comap_const_of_notMem (since := "2025-05-23")]

theorem Filter.comap_const_of_not_mem {α : Type u_1} {β : Type u_2} {g : Filter β} {t : Set β} {x : β} (ht : t ∈ g) (hx : x ∉ t) : comap (fun (x_1 : α) => x) g = ⊥

Alias of Filter.comap_const_of_notMem.

theorem Filter.comap_const_of_mem {α : Type u_1} {β : Type u_2} {g : Filter β} {x : β} (h : ∀ t ∈ g, x ∈ t) : comap (fun (x_1 : α) => x) g = ⊤

theorem Filter.map_const {α : Type u_1} {β : Type u_2} {f : Filter α} [f.NeBot] {c : β} : map (fun (x : α) => c) f = pure c

theorem Filter.comap_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : γ → β} {n : β → α} : comap m (comap n f) = comap (n ∘ m) f

The variables in the following lemmas are used as in this diagram:

    φ
  α → β
θ ↓   ↓ ψ
  γ → δ
    ρ

theorem Filter.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ) (F : Filter α) : map ψ (map φ F) = map ρ (map θ F)

theorem Filter.comap_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ) (G : Filter δ) : comap φ (comap ψ G) = comap θ (comap ρ G)

theorem Function.Semiconj.filter_map {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) : Semiconj (Filter.map f) (Filter.map ga) (Filter.map gb)

theorem Function.Commute.filter_map {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Function.Commute (Filter.map f) (Filter.map g)

theorem Function.Semiconj.filter_comap {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) : Semiconj (Filter.comap f) (Filter.comap gb) (Filter.comap ga)

theorem Function.Commute.filter_comap {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Function.Commute (Filter.comap f) (Filter.comap g)

theorem Function.LeftInverse.filter_map {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : LeftInverse g f) : LeftInverse (Filter.map g) (Filter.map f)

theorem Function.LeftInverse.filter_comap {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : LeftInverse g f) : RightInverse (Filter.comap g) (Filter.comap f)

theorem Function.RightInverse.filter_map {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : RightInverse g f) : RightInverse (Filter.map g) (Filter.map f)

theorem Function.RightInverse.filter_comap {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : RightInverse g f) : LeftInverse (Filter.comap g) (Filter.comap f)

theorem Set.LeftInvOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {g : β → α} (hfg : LeftInvOn g f s) : LeftInvOn (Filter.map g) (Filter.map f) (Iic (Filter.principal s))

theorem Set.RightInvOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {g : β → α} (hfg : RightInvOn g f t) : RightInvOn (Filter.map g) (Filter.map f) (Iic (Filter.principal t))

def Filter.kernMap {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter α) : Filter β

The analog of Set.kernImage for filters. A set s belongs to Filter.kernMap m f if either of the following equivalent conditions hold.

1. There exists a set t ∈ f such that s = Set.kernImage m t. This is used as a definition.
2. There exists a set t such that tᶜ ∈ f and sᶜ = m '' t, see Filter.mem_kernMap_iff_compl and Filter.compl_mem_kernMap.

This definition is useful because it gives a right adjoint to Filter.comap, and because it has a nice interpretation when working with co- filters (Filter.cocompact, Filter.cofinite, ...). For example, kernMap m (cocompact α) is the filter generated by the complements of the sets m '' K where K is a compact subset of α.

Equations

• Filter.kernMap m f = { sets := Set.kernImage m '' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.mem_kernMap {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β} : s ∈ kernMap m f ↔ ∃ t ∈ f, Set.kernImage m t = s

theorem Filter.mem_kernMap_iff_compl {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β} : s ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ

theorem Filter.compl_mem_kernMap {α : Type u_1} {β : Type u_2} {m : α → β} {f : Filter α} {s : Set β} : sᶜ ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s

theorem Filter.comap_le_iff_le_kernMap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {f : Filter α} : comap m g ≤ f ↔ g ≤ kernMap m f

theorem Filter.gc_comap_kernMap {α : Type u_1} {β : Type u_2} (m : α → β) : GaloisConnection (comap m) (kernMap m)

theorem Filter.kernMap_principal {α : Type u_1} {β : Type u_2} {m : α → β} {s : Set α} : kernMap m (principal s) = principal (Set.kernImage m s)

@[simp]

theorem Filter.comap_principal {α : Type u_1} {β : Type u_2} {m : α → β} {t : Set β} : comap m (principal t) = principal (m ⁻¹' t)

theorem Filter.principal_subtype {α : Type u_6} (s : Set α) (t : Set ↑s) : principal t = comap Subtype.val (principal (Subtype.val '' t))

@[simp]

theorem Filter.comap_pure {α : Type u_1} {β : Type u_2} {m : α → β} {b : β} : comap m (pure b) = principal (m ⁻¹' {b})

theorem Filter.map_le_iff_le_comap {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {m : α → β} : map m f ≤ g ↔ f ≤ comap m g

theorem Filter.gc_map_comap {α : Type u_1} {β : Type u_2} (m : α → β) : GaloisConnection (map m) (comap m)

theorem Filter.map_mono {α : Type u_1} {β : Type u_2} {m : α → β} : Monotone (map m)

theorem Filter.comap_mono {α : Type u_1} {β : Type u_2} {m : α → β} : Monotone (comap m)

theorem GCongr.Filter.map_le_map {α : Type u_1} {β : Type u_2} {m : α → β} {F G : Filter α} (h : F ≤ G) : Filter.map m F ≤ Filter.map m G

Temporary lemma that we can tag with gcongr

theorem GCongr.Filter.comap_le_comap {α : Type u_1} {β : Type u_2} {m : α → β} {F G : Filter β} (h : F ≤ G) : Filter.comap m F ≤ Filter.comap m G

Temporary lemma that we can tag with gcongr

@[simp]

theorem Filter.map_bot {α : Type u_1} {β : Type u_2} {m : α → β} : map m ⊥ = ⊥

@[simp]

theorem Filter.map_sup {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {m : α → β} : map m (f₁ ⊔ f₂) = map m f₁ ⊔ map m f₂

@[simp]

theorem Filter.map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {m : α → β} {f : ι → Filter α} : map m (⨆ (i : ι), f i) = ⨆ (i : ι), map m (f i)

@[simp]

theorem Filter.map_top {α : Type u_1} {β : Type u_2} (f : α → β) : map f ⊤ = principal (Set.range f)

@[simp]

theorem Filter.comap_top {α : Type u_1} {β : Type u_2} {m : α → β} : comap m ⊤ = ⊤

@[simp]

theorem Filter.comap_inf {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β} : comap m (g₁ ⊓ g₂) = comap m g₁ ⊓ comap m g₂

@[simp]

theorem Filter.comap_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {m : α → β} {f : ι → Filter β} : comap m (⨅ (i : ι), f i) = ⨅ (i : ι), comap m (f i)

theorem Filter.le_comap_top {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter α) : l ≤ comap f ⊤

theorem Filter.map_comap_le {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} : map m (comap m g) ≤ g

theorem Filter.le_comap_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : f ≤ comap m (map m f)

@[simp]

theorem Filter.comap_bot {α : Type u_1} {β : Type u_2} {m : α → β} : comap m ⊥ = ⊥

theorem Filter.neBot_of_comap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} (h : (comap m g).NeBot) : g.NeBot

theorem Filter.comap_inf_principal_range {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} : comap m (g ⊓ principal (Set.range m)) = comap m g

theorem Filter.disjoint_comap {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β} (h : Disjoint g₁ g₂) : Disjoint (comap m g₁) (comap m g₂)

theorem Filter.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : ι → Filter β} {m : α → β} : comap m (iSup f) = ⨆ (i : ι), comap m (f i)

theorem Filter.comap_sSup {α : Type u_1} {β : Type u_2} {s : Set (Filter β)} {m : α → β} : comap m (sSup s) = ⨆ f ∈ s, comap m f

theorem Filter.comap_sup {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β} : comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

theorem Filter.map_comap {α : Type u_1} {β : Type u_2} (f : Filter β) (m : α → β) : map m (comap m f) = f ⊓ principal (Set.range m)

theorem Filter.map_comap_setCoe_val {β : Type u_2} (f : Filter β) (s : Set β) : map Subtype.val (comap Subtype.val f) = f ⊓ principal s

theorem Filter.map_comap_of_mem {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hf : Set.range m ∈ f) : map m (comap m f) = f

instance Filter.canLift {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Filter α) (Filter β) (map c) fun (f : Filter α) => ∀ᶠ (x : α) in f, p x

theorem Filter.comap_le_comap_iff {α : Type u_1} {β : Type u_2} {f g : Filter β} {m : α → β} (hf : Set.range m ∈ f) : comap m f ≤ comap m g ↔ f ≤ g

theorem Filter.map_comap_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) (l : Filter β) : map f (comap f l) = l

theorem Filter.comap_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) : Function.Injective (comap f)

theorem Function.Surjective.filter_map_top {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) : Filter.map f ⊤ = ⊤

theorem Filter.subtype_coe_map_comap {α : Type u_1} (s : Set α) (f : Filter α) : map Subtype.val (comap Subtype.val f) = f ⊓ principal s

theorem Filter.image_mem_of_mem_comap {α : Type u_1} {β : Type u_2} {f : Filter α} {c : β → α} (h : Set.range c ∈ f) {W : Set β} (W_in : W ∈ comap c f) : c '' W ∈ f

theorem Filter.image_coe_mem_of_mem_comap {α : Type u_1} {f : Filter α} {U : Set α} (h : U ∈ f) {W : Set ↑U} (W_in : W ∈ comap Subtype.val f) : Subtype.val '' W ∈ f

theorem Filter.comap_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} (h : Function.Injective m) : comap m (map m f) = f

theorem Filter.mem_comap_iff {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (inj : Function.Injective m) (large : Set.range m ∈ f) {S : Set α} : S ∈ comap m f ↔ m '' S ∈ f

theorem Filter.map_le_map_iff_of_injOn {α : Type u_1} {β : Type u_2} {l₁ l₂ : Filter α} {f : α → β} {s : Set α} (h₁ : s ∈ l₁) (h₂ : s ∈ l₂) (hinj : Set.InjOn f s) : map f l₁ ≤ map f l₂ ↔ l₁ ≤ l₂

theorem Filter.map_le_map_iff {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (hm : Function.Injective m) : map m f ≤ map m g ↔ f ≤ g

theorem Filter.map_eq_map_iff_of_injOn {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {s : Set α} (hsf : s ∈ f) (hsg : s ∈ g) (hm : Set.InjOn m s) : map m f = map m g ↔ f = g

theorem Filter.map_inj {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (hm : Function.Injective m) : map m f = map m g ↔ f = g

theorem Filter.map_injective {α : Type u_1} {β : Type u_2} {m : α → β} (hm : Function.Injective m) : Function.Injective (map m)

theorem Filter.comap_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : (comap m f).NeBot ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t

theorem Filter.comap_neBot {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hm : ∀ t ∈ f, ∃ (a : α), m a ∈ t) : (comap m f).NeBot

theorem Filter.comap_neBot_iff_frequently {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : (comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ Set.range m

theorem Filter.comap_neBot_iff_compl_range {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : (comap m f).NeBot ↔ (Set.range m)ᶜ ∉ f

theorem Filter.comap_eq_bot_iff_compl_range {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : comap m f = ⊥ ↔ (Set.range m)ᶜ ∈ f

theorem Filter.comap_surjective_eq_bot {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hm : Function.Surjective m) : comap m f = ⊥ ↔ f = ⊥

theorem Filter.disjoint_comap_iff {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β} (h : Function.Surjective m) : Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂

theorem Filter.NeBot.comap_of_range_mem {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : f.NeBot → ∀ (hm : Set.range m ∈ f), (comap m f).NeBot

@[simp]

theorem Filter.comap_inl_map_inr {α : Type u_1} {β : Type u_2} {g : Filter β} : comap Sum.inl (map Sum.inr g) = ⊥

@[simp]

theorem Filter.comap_inr_map_inl {α : Type u_1} {β : Type u_2} {f : Filter α} : comap Sum.inr (map Sum.inl f) = ⊥

@[simp]

theorem Filter.map_inl_inf_map_inr {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : map Sum.inl f ⊓ map Sum.inr g = ⊥

@[simp]

theorem Filter.map_inr_inf_map_inl {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : map Sum.inr f ⊓ map Sum.inl g = ⊥

theorem Filter.comap_sumElim_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter γ) (m₁ : α → γ) (m₂ : β → γ) : comap (Sum.elim m₁ m₂) l = map Sum.inl (comap m₁ l) ⊔ map Sum.inr (comap m₂ l)

theorem Filter.map_comap_inl_sup_map_comap_inr {α : Type u_1} {β : Type u_2} (l : Filter (α ⊕ β)) : map Sum.inl (comap Sum.inl l) ⊔ map Sum.inr (comap Sum.inr l) = l

theorem Filter.map_sumElim_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter (α ⊕ β)) (m₁ : α → γ) (m₂ : β → γ) : map (Sum.elim m₁ m₂) l = map m₁ (comap Sum.inl l) ⊔ map m₂ (comap Sum.inr l)

@[simp]

theorem Filter.comap_fst_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} : (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

instance Filter.comap_fst_neBot {α : Type u_1} {β : Type u_2} [Nonempty β] {f : Filter α} [f.NeBot] : (comap Prod.fst f).NeBot

@[simp]

theorem Filter.comap_snd_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter β} : (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

instance Filter.comap_snd_neBot {α : Type u_1} {β : Type u_2} [Nonempty α] {f : Filter β} [f.NeBot] : (comap Prod.snd f).NeBot

theorem Filter.comap_eval_neBot_iff' {ι : Type u_6} {α : ι → Type u_7} {i : ι} {f : Filter (α i)} : (comap (Function.eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

@[simp]

theorem Filter.comap_eval_neBot_iff {ι : Type u_6} {α : ι → Type u_7} [∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)} : (comap (Function.eval i) f).NeBot ↔ f.NeBot

instance Filter.comap_eval_neBot {ι : Type u_6} {α : ι → Type u_7} [∀ (j : ι), Nonempty (α j)] (i : ι) (f : Filter (α i)) [f.NeBot] : (comap (Function.eval i) f).NeBot

theorem Filter.comap_coe_neBot_of_le_principal {γ : Type u_3} {s : Set γ} {l : Filter γ} [h : l.NeBot] (h' : l ≤ principal s) : (comap Subtype.val l).NeBot

theorem Filter.NeBot.comap_of_surj {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hf : f.NeBot) (hm : Function.Surjective m) : (comap m f).NeBot

theorem Filter.NeBot.comap_of_image_mem {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hf : f.NeBot) {s : Set α} (hs : m '' s ∈ f) : (comap m f).NeBot

@[simp]

theorem Filter.map_eq_bot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : map m f = ⊥ ↔ f = ⊥

theorem Filter.map_neBot_iff {α : Type u_1} {β : Type u_2} (f : α → β) {F : Filter α} : (map f F).NeBot ↔ F.NeBot

theorem Filter.NeBot.map {α : Type u_1} {β : Type u_2} {f : Filter α} (hf : f.NeBot) (m : α → β) : (Filter.map m f).NeBot

theorem Filter.NeBot.of_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : (Filter.map m f).NeBot → f.NeBot

instance Filter.map_neBot {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} [hf : f.NeBot] : (map m f).NeBot

theorem Filter.sInter_comap_sets {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter β) : ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

theorem Filter.map_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β} : map m (iInf f) ≤ ⨅ (i : ι), map m (f i)

theorem Filter.map_iInf_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β} (hf : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) [Nonempty ι] : map m (iInf f) = ⨅ (i : ι), map m (f i)

theorem Filter.map_biInf_eq {α : Type u_1} {β : Type u_2} {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 ≥ x2) {x : ι | p x}) (ne : ∃ (i : ι), p i) : map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), map m (f i)

theorem Filter.map_inf_le {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} : map m (f ⊓ g) ≤ map m f ⊓ map m g

theorem Filter.map_inf {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (h : Function.Injective m) : map m (f ⊓ g) = map m f ⊓ map m g

theorem Filter.map_inf' {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g) (h : Set.InjOn m t) : map m (f ⊓ g) = map m f ⊓ map m g

theorem Filter.disjoint_of_map {α : Type u_6} {β : Type u_7} {F G : Filter α} {f : α → β} (h : Disjoint (map f F) (map f G)) : Disjoint F G

theorem Filter.disjoint_map {α : Type u_1} {β : Type u_2} {m : α → β} (hm : Function.Injective m) {f₁ f₂ : Filter α} : Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

theorem Filter.map_equiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter β) : map (⇑e.symm) f = comap (⇑e) f

theorem Filter.map_eq_comap_of_inverse {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {n : β → α} (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) : map m f = comap n f

theorem Filter.comap_equiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter α) : comap (⇑e.symm) f = map (⇑e) f

theorem Filter.map_swap_eq_comap_swap {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} : map Prod.swap f = comap Prod.swap f

theorem Filter.map_swap4_eq_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter ((α × β) × γ × δ)} : map (fun (p : (α × β) × γ × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) f = comap (fun (p : (α × γ) × β × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) f

A useful lemma when dealing with uniformities.

theorem Filter.le_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β} (h : ∀ s ∈ f, m '' s ∈ g) : g ≤ map m f

theorem Filter.le_map_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β} : g ≤ map m f ↔ ∀ s ∈ f, m '' s ∈ g

theorem Filter.push_pull {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β) : map f (F ⊓ comap f G) = map f F ⊓ G

theorem Filter.push_pull' {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β) : map f (comap f G ⊓ F) = G ⊓ map f F

theorem Filter.disjoint_comap_iff_map {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : Disjoint F (comap f G) ↔ Disjoint (map f F) G

theorem Filter.disjoint_comap_iff_map' {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : Disjoint (comap f G) F ↔ Disjoint G (map f F)

theorem Filter.neBot_inf_comap_iff_map {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot

theorem Filter.neBot_inf_comap_iff_map' {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot

theorem Filter.comap_inf_principal_neBot_of_image_mem {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hf : f.NeBot) {s : Set α} (hs : m '' s ∈ f) : (comap m f ⊓ principal s).NeBot

theorem Filter.principal_eq_map_coe_top {α : Type u_1} (s : Set α) : principal s = map Subtype.val ⊤

theorem Filter.inf_principal_eq_bot_iff_comap {α : Type u_1} {F : Filter α} {s : Set α} : F ⊓ principal s = ⊥ ↔ comap Subtype.val F = ⊥

theorem Filter.map_generate_le_generate_preimage_preimage {α : Type u_1} {β : Type u_2} (U : Set (Set β)) (f : β → α) : map f (generate U) ≤ generate ((fun (x : Set α) => f ⁻¹' x) ⁻¹' U)

theorem Filter.generate_image_preimage_le_comap {α : Type u_1} {β : Type u_2} (U : Set (Set α)) (f : β → α) : generate ((fun (x : Set α) => f ⁻¹' x) '' U) ≤ comap f (generate U)

theorem Filter.singleton_mem_pure {α : Type u_1} {a : α} : {a} ∈ pure a

theorem Filter.pure_injective {α : Type u_1} : Function.Injective pure

instance Filter.pure_neBot {α : Type u} {a : α} : (pure a).NeBot

@[simp]

theorem Filter.le_pure_iff {α : Type u_1} {f : Filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f

theorem Filter.mem_seq_def {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set β} : s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, x y ∈ s

theorem Filter.mem_seq_iff {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set β} : s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

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

theorem Filter.seq_mem_seq {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {s : Set (α → β)} {t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s.seq t ∈ f.seq g

theorem Filter.le_seq {α : Type u_1} {β : Type u_2} {f : Filter (α → β)} {g : Filter α} {h : Filter β} (hh : ∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h) : h ≤ f.seq g

theorem Filter.seq_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter (α → β)} {g₁ g₂ : Filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.seq g₁ ≤ f₂.seq g₂

@[simp]

theorem Filter.pure_seq_eq_map {α : Type u_1} {β : Type u_2} (g : α → β) (f : Filter α) : (pure g).seq f = map g f

@[simp]

theorem Filter.seq_pure {α : Type u_1} {β : Type u_2} (f : Filter (α → β)) (a : α) : f.seq (pure a) = map (fun (g : α → β) => g a) f

@[simp]

theorem Filter.seq_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)) : h.seq (g.seq x) = ((map (fun (x1 : β → γ) (x2 : α → β) => x1 ∘ x2) h).seq g).seq x

theorem Filter.prod_map_seq_comm {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : (map Prod.mk f).seq g = (map (fun (b : β) (a : α) => (a, b)) g).seq f

theorem Filter.seq_eq_filter_seq {α β : Type u} (f : Filter (α → β)) (g : Filter α) : f <*> g = f.seq g

instance Filter.instLawfulApplicative : LawfulApplicative Filter

instance Filter.instCommApplicative : CommApplicative Filter

bind equations

@[simp]

theorem Filter.eventually_bind {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → Filter β} {p : β → Prop} : (∀ᶠ (y : β) in f.bind m, p y) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y

@[simp]

theorem Filter.frequently_bind {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → Filter β} {p : β → Prop} : (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

@[simp]

theorem Filter.eventuallyEq_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} : g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂

@[simp]

theorem Filter.eventuallyLE_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} : g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂

theorem Filter.mem_bind' {α : Type u_1} {β : Type u_2} {s : Set β} {f : Filter α} {m : α → Filter β} : s ∈ f.bind m ↔ {a : α | s ∈ m a} ∈ f

@[simp]

theorem Filter.mem_bind {α : Type u_1} {β : Type u_2} {s : Set β} {f : Filter α} {m : α → Filter β} : s ∈ f.bind m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x

theorem Filter.bind_le {α : Type u_1} {β : Type u_2} {f : Filter α} {g : α → Filter β} {l : Filter β} (h : ∀ᶠ (x : α) in f, g x ≤ l) : f.bind g ≤ l

theorem Filter.bind_mono {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : α → Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) : f₁.bind g₁ ≤ f₂.bind g₂

theorem Filter.bind_inf_principal {α : Type u_1} {β : Type u_2} {f : Filter α} {g : α → Filter β} {s : Set β} : (f.bind fun (x : α) => g x ⊓ principal s) = f.bind g ⊓ principal s

theorem Filter.sup_bind {α : Type u_1} {β : Type u_2} {f g : Filter α} {h : α → Filter β} : (f ⊔ g).bind h = f.bind h ⊔ g.bind h

theorem Filter.principal_bind {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → Filter β} : (principal s).bind f = ⨆ x ∈ s, f x

theorem Filter.map_surjOn_Iic_iff_le_map {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.SurjOn (map m) (Set.Iic F) (Set.Iic G) ↔ G ≤ map m F

theorem Filter.map_surjOn_Iic_iff_surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.SurjOn (map m) (Set.Iic (principal s)) (Set.Iic (principal t)) ↔ Set.SurjOn m s t

theorem Set.SurjOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : SurjOn m s t → SurjOn (Filter.map m) (Iic (Filter.principal s)) (Iic (Filter.principal t))

Alias of the reverse direction of Filter.map_surjOn_Iic_iff_surjOn.

theorem Filter.filter_injOn_Iic_iff_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : Set.InjOn (map m) (Set.Iic (principal s)) ↔ Set.InjOn m s

theorem Set.InjOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : InjOn m s → InjOn (Filter.map m) (Iic (Filter.principal s))

Alias of the reverse direction of Filter.filter_injOn_Iic_iff_injOn.