# Theorems about map and comap on filters. #

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

source
@[simp]
theorem Filter.map_principal {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} :
map f (principal s) = principal (f '' s)
source
@[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)
source
@[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)
source
@[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
source
@[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
source
@[simp]
theorem Filter.mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} :
t ∈ map m f ↔ m ⁻¹' t ∈ f
source
theorem Filter.mem_map' {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} :
t ∈ map m f ↔ {x : α | m x ∈ t} ∈ f
source
theorem Filter.image_mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α} (hs : s ∈ f) :
m '' s ∈ map m f
source
@[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
source
theorem Filter.range_mem_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} :
Set.range m ∈ map m f
source
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
source
@[simp]
theorem Filter.map_id {α : Type u_1} {f : Filter α} :
map id f = f
source
@[simp]
theorem Filter.map_id' {α : Type u_1} {f : Filter α} :
map (fun (x : α) => x) f = f
source
@[simp]
theorem Filter.map_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : α → β} {m' : β → γ} :
map m' ∘ map m = map (m' ∘ m)
source
@[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
source
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.

source
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
source
theorem Filter.mem_comap'' {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} :
s ∈ comap f l ↔ Set.kernImage f s ∈ l
source
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`.

source
@[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
source
@[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
source
theorem Filter.mem_comap_iff_compl {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} :
s ∈ comap f l ↔ (f '' s ᶜ)ᶜ ∈ l
source
theorem Filter.compl_mem_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α} :
s ᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l
source
instance Filter.instLawfulFunctor :
LawfulFunctor Filter
source
theorem Filter.pure_sets {α : Type u_1} (a : α) :
(pure a).sets = {s : Set α | a ∈ s}
source
@[simp]
theorem Filter.eventually_pure {α : Type u_1} {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in pure a, p x) ↔ p a
source
@[simp]
theorem Filter.principal_singleton {α : Type u_1} (a : α) :
principal {a} = pure a
source
@[simp]
theorem Filter.biSup_pure_eq_principal {α : Type u_1} (s : Set α) :
⨆ a ∈ s, pure a = principal s
source
@[simp]
theorem Filter.iSup_pure_eq_top {α : Type u_1} :
⨆ (a : α), pure a = ⊤
source
@[simp]
theorem Filter.map_pure {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
map f (pure a) = pure (f a)
source
theorem Filter.pure_le_principal {α : Type u_1} {s : Set α} (a : α) :
pure a ≤ principal s ↔ a ∈ s
source
@[simp]
theorem Filter.join_pure {α : Type u_1} (f : Filter α) :
(pure f).join = f
source
@[simp]
theorem Filter.pure_bind {α : Type u_1} {β : Type u_2} (a : α) (m : α → Filter β) :
(pure a).bind m = m a
source
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)
source
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 `Filter`s. 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`.

source
def Filter.monad :
Monad Filter

The monad structure on filters.

Equations

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

Instances For

source
theorem Filter.lawfulMonad :
LawfulMonad Filter
source
instance Filter.instAlternative :
Alternative Filter
Equations

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

source
@[simp]
theorem Filter.map_def {α β : Type u_6} (m : α → β) (f : Filter α) :
m <$> f = map m f
source
@[simp]
theorem Filter.bind_def {α β : Type u_6} (f : Filter α) (m : α → Filter β) :
f >>= m = f.bind m

#### `map` and `comap` equations #

source
@[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
source
theorem Filter.preimage_mem_comap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} {t : Set β} (ht : t ∈ g) :
m ⁻¹' t ∈ comap m g
source
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)
source
theorem Filter.comap_id {α : Type u_1} {f : Filter α} :
comap id f = f
source
theorem Filter.comap_id' {α : Type u_1} {f : Filter α} :
comap (fun (x : α) => x) f = f
source
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 = ⊥
source
@[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`.

source
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 = ⊤
source
theorem Filter.map_const {α : Type u_1} {β : Type u_2} {f : Filter α} [f.NeBot] {c : β} :
map (fun (x : α) => c) f = pure c
source
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:

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

source
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)
source
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)
source
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)
source
theorem Function.Commute.filter_map {α : Type u_1} {f g : α → α} (h : Function.Commute f g) :
Function.Commute (Filter.map f) (Filter.map g)
source
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)
source
theorem Function.Commute.filter_comap {α : Type u_1} {f g : α → α} (h : Function.Commute f g) :
Function.Commute (Filter.comap f) (Filter.comap g)
source
theorem Function.LeftInverse.filter_map {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : LeftInverse g f) :
LeftInverse (Filter.map g) (Filter.map f)
source
theorem Function.LeftInverse.filter_comap {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : LeftInverse g f) :
RightInverse (Filter.comap g) (Filter.comap f)
source
theorem Function.RightInverse.filter_map {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : RightInverse g f) :
RightInverse (Filter.map g) (Filter.map f)
source
theorem Function.RightInverse.filter_comap {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : RightInverse g f) :
LeftInverse (Filter.comap g) (Filter.comap f)
source
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))
source
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))
source
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 := ⋯ }

Instances For

source
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
source
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 ᶜ
source
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
source
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
source
theorem Filter.gc_comap_kernMap {α : Type u_1} {β : Type u_2} (m : α → β) :
GaloisConnection (comap m) (kernMap m)
source
theorem Filter.kernMap_principal {α : Type u_1} {β : Type u_2} {m : α → β} {s : Set α} :
kernMap m (principal s) = principal (Set.kernImage m s)
source
@[simp]
theorem Filter.comap_principal {α : Type u_1} {β : Type u_2} {m : α → β} {t : Set β} :
comap m (principal t) = principal (m ⁻¹' t)
source
theorem Filter.principal_subtype {α : Type u_6} (s : Set α) (t : Set ↑s) :
principal t = comap Subtype.val (principal (Subtype.val '' t))
source
@[simp]
theorem Filter.comap_pure {α : Type u_1} {β : Type u_2} {m : α → β} {b : β} :
comap m (pure b) = principal (m ⁻¹' {b})
source
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
source
theorem Filter.gc_map_comap {α : Type u_1} {β : Type u_2} (m : α → β) :
GaloisConnection (map m) (comap m)
source
theorem Filter.map_mono {α : Type u_1} {β : Type u_2} {m : α → β} :
Monotone (map m)
source
theorem Filter.comap_mono {α : Type u_1} {β : Type u_2} {m : α → β} :
Monotone (comap m)
source
@[simp]
theorem Filter.map_bot {α : Type u_1} {β : Type u_2} {m : α → β} :
map m ⊥ = ⊥
source
@[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₂
source
@[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)
source
@[simp]
theorem Filter.map_top {α : Type u_1} {β : Type u_2} (f : α → β) :
map f ⊤ = principal (Set.range f)
source
@[simp]
theorem Filter.comap_top {α : Type u_1} {β : Type u_2} {m : α → β} :
comap m ⊤ = ⊤
source
@[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₂
source
@[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)
source
theorem Filter.le_comap_top {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter α) :
l ≤ comap f ⊤
source
theorem Filter.map_comap_le {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} :
map m (comap m g) ≤ g
source
theorem Filter.le_comap_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} :
f ≤ comap m (map m f)
source
@[simp]
theorem Filter.comap_bot {α : Type u_1} {β : Type u_2} {m : α → β} :
comap m ⊥ = ⊥
source
theorem Filter.neBot_of_comap {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} (h : (comap m g).NeBot) :
g.NeBot
source
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
source
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₂)
source
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)
source
theorem Filter.comap_sSup {α : Type u_1} {β : Type u_2} {s : Set (Filter β)} {m : α → β} :
comap m (sSup s) = ⨆ f ∈ s, comap m f
source
theorem Filter.comap_sup {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β} :
comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
source
theorem Filter.map_comap {α : Type u_1} {β : Type u_2} (f : Filter β) (m : α → β) :
map m (comap m f) = f ⊓ principal (Set.range m)
source
theorem Filter.map_comap_setCoe_val {β : Type u_2} (f : Filter β) (s : Set β) :
map Subtype.val (comap Subtype.val f) = f ⊓ principal s
source
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
source
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
source
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
source
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
source
theorem Filter.comap_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) :
Function.Injective (comap f)
source
theorem Function.Surjective.filter_map_top {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) :
Filter.map f ⊤ = ⊤
source
theorem Filter.subtype_coe_map_comap {α : Type u_1} (s : Set α) (f : Filter α) :
map Subtype.val (comap Subtype.val f) = f ⊓ principal s
source
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
source
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
source
theorem Filter.comap_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} (h : Function.Injective m) :
comap m (map m f) = f
source
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
source
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₂
source
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
source
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
source
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
source
theorem Filter.map_injective {α : Type u_1} {β : Type u_2} {m : α → β} (hm : Function.Injective m) :
Function.Injective (map m)
source
theorem Filter.comap_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} :
(comap m f).NeBot ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t
source
theorem Filter.comap_neBot {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hm : ∀ t ∈ f, ∃ (a : α), m a ∈ t) :
(comap m f).NeBot
source
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
source
theorem Filter.comap_neBot_iff_compl_range {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} :
(comap m f).NeBot ↔ (Set.range m)ᶜ ∉ f
source
theorem Filter.comap_eq_bot_iff_compl_range {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} :
comap m f = ⊥ ↔ (Set.range m)ᶜ ∈ f
source
theorem Filter.comap_surjective_eq_bot {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hm : Function.Surjective m) :
comap m f = ⊥ ↔ f = ⊥
source
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₂
source
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
source
@[simp]
theorem Filter.comap_inl_map_inr {α : Type u_1} {β : Type u_2} {g : Filter β} :
comap Sum.inl (map Sum.inr g) = ⊥
source
@[simp]
theorem Filter.comap_inr_map_inl {α : Type u_1} {β : Type u_2} {f : Filter α} :
comap Sum.inr (map Sum.inl f) = ⊥
source
@[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 = ⊥
source
@[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 = ⊥
source
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)
source
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
source
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)
source
@[simp]
theorem Filter.comap_fst_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} :
(comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
source
instance Filter.comap_fst_neBot {α : Type u_1} {β : Type u_2} [Nonempty β] {f : Filter α} [f.NeBot] :
(comap Prod.fst f).NeBot
source
@[simp]
theorem Filter.comap_snd_neBot_iff {α : Type u_1} {β : Type u_2} {f : Filter β} :
(comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
source
instance Filter.comap_snd_neBot {α : Type u_1} {β : Type u_2} [Nonempty α] {f : Filter β} [f.NeBot] :
(comap Prod.snd f).NeBot
source
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
source
@[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
source
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
source
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
source
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
source
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
source
@[simp]
theorem Filter.map_eq_bot_iff {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} :
map m f = ⊥ ↔ f = ⊥
source
theorem Filter.map_neBot_iff {α : Type u_1} {β : Type u_2} (f : α → β) {F : Filter α} :
(map f F).NeBot ↔ F.NeBot
source
theorem Filter.NeBot.map {α : Type u_1} {β : Type u_2} {f : Filter α} (hf : f.NeBot) (m : α → β) :
(Filter.map m f).NeBot
source
theorem Filter.NeBot.of_map {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} :
(Filter.map m f).NeBot → f.NeBot
source
instance Filter.map_neBot {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} [hf : f.NeBot] :
(map m f).NeBot
source
theorem Filter.sInter_comap_sets {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter β) :
⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U
source
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)
source
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)
source
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)
source
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
source
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
source
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
source
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
source
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₂
source
theorem Filter.map_equiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter β) :
map (⇑e.symm) f = comap (⇑e) f
source
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
source
theorem Filter.comap_equiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter α) :
comap (⇑e.symm) f = map (⇑e) f
source
theorem Filter.map_swap_eq_comap_swap {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} :
map Prod.swap f = comap Prod.swap f
source
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.

source
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
source
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
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
theorem Filter.principal_eq_map_coe_top {α : Type u_1} (s : Set α) :
principal s = map Subtype.val ⊤
source
theorem Filter.inf_principal_eq_bot_iff_comap {α : Type u_1} {F : Filter α} {s : Set α} :
F ⊓ principal s = ⊥ ↔ comap Subtype.val F = ⊥
source
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)
source
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)
source
theorem Filter.singleton_mem_pure {α : Type u_1} {a : α} :
{a} ∈ pure a
source
theorem Filter.pure_injective {α : Type u_1} :
Function.Injective pure
source
instance Filter.pure_neBot {α : Type u} {a : α} :
(pure a).NeBot
source
@[simp]
theorem Filter.le_pure_iff {α : Type u_1} {f : Filter α} {a : α} :
f ≤ pure a ↔ {a} ∈ f
source
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
source
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
source
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
source
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
source
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
source
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₂
source
@[simp]
theorem Filter.pure_seq_eq_map {α : Type u_1} {β : Type u_2} (g : α → β) (f : Filter α) :
(pure g).seq f = map g f
source
@[simp]
theorem Filter.seq_pure {α : Type u_1} {β : Type u_2} (f : Filter (α → β)) (a : α) :
f.seq (pure a) = map (fun (g : α → β) => g a) f
source
@[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
source
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
source
theorem Filter.seq_eq_filter_seq {α β : Type u} (f : Filter (α → β)) (g : Filter α) :
f <*> g = f.seq g
source
instance Filter.instLawfulApplicative :
LawfulApplicative Filter
source
instance Filter.instCommApplicative :
CommApplicative Filter

#### `bind` equations #

source
@[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
source
@[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
source
@[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₂
source
@[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₂
source
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
source
@[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
source
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
source
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₂
source
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
source
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
source
theorem Filter.principal_bind {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → Filter β} :
(principal s).bind f = ⨆ x ∈ s, f x
source
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
source
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
source
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`.

source
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
source
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`.