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.

@[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.frequently_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.biSup_pure_eq_principal {α : Type u_1} (s : Set α) : ⨆ a ∈ s, pure a = principal s

@[simp]

theorem Filter.iSup_pure_eq_top {α : Type u_1} : ⨆ (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.

@[implicit_reducible]

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

@[implicit_reducible]

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 = ⊥

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)

@[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 = ⊥

@[simp]

theorem Filter.bot_eq_map_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.