Loogle!

Result

Found 501 declarations mentioning Filter.map. Of these, only the first 200 are shown.

• Filter.map 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter α) : Filter β
• Filter.map_id 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {f : Filter α} : Filter.map id f = f
• Filter.map_id' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {f : Filter α} : Filter.map (fun x => x) f = f
• Filter.map_neBot 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} [hf : f.NeBot] : (Filter.map m f).NeBot
• Filter.NeBot.map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} (hf : f.NeBot) (m : α → β) : (Filter.map m f).NeBot
• Filter.NeBot.of_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : (Filter.map m f).NeBot → f.NeBot
• Filter.map_injective 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m : α → β} (hm : Function.Injective m) : Function.Injective (Filter.map m)
• Filter.map_neBot_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : α → β) {F : Filter α} : (Filter.map f F).NeBot ↔ F.NeBot
• Function.Commute.filter_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Function.Commute (Filter.map f) (Filter.map g)
• Filter.map_bot 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m : α → β} : Filter.map m ⊥ = ⊥
• Filter.map_def 📋 Mathlib.Order.Filter.Map
  {α β : Type u_6} (m : α → β) (f : Filter α) : m <$> f = Filter.map m f
• Filter.map_const 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} [f.NeBot] {c : β} : Filter.map (fun x => c) f = pure c
• Filter.map_top 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : α → β) : Filter.map f ⊤ = Filter.principal (Set.range f)
• Filter.range_mem_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : Set.range m ∈ Filter.map m f
• Filter.comap_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} (h : Function.Injective m) : Filter.comap m (Filter.map m f) = f
• Filter.map_comap_of_surjective 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) (l : Filter β) : Filter.map f (Filter.comap f l) = l
• Filter.map_mono 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m : α → β} : Monotone (Filter.map m)
• Filter.map_principal 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : Filter.map f (Filter.principal s) = Filter.principal (f '' s)
• Filter.map_pure 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : Filter.map f (pure a) = pure (f a)
• Filter.bind.eq_1 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : Filter α) (m : α → Filter β) : f.bind m = (Filter.map m f).join
• Filter.pure_seq_eq_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (g : α → β) (f : Filter α) : (pure g).seq f = Filter.map g f
• Function.LeftInverse.filter_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : Function.LeftInverse g f) : Function.LeftInverse (Filter.map g) (Filter.map f)
• Function.RightInverse.filter_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hfg : Function.RightInverse g f) : Function.RightInverse (Filter.map g) (Filter.map f)
• Function.Surjective.filter_map_top 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) : Filter.map f ⊤ = ⊤
• Filter.eventually_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop} : (∀ᶠ (b : β) in Filter.map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)
• Filter.frequently_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop} : (∃ᶠ (b : β) in Filter.map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)
• Filter.gc_map_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (m : α → β) : GaloisConnection (Filter.map m) (Filter.comap m)
• Filter.le_comap_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : f ≤ Filter.comap m (Filter.map m f)
• Filter.map_comap_le 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β} : Filter.map m (Filter.comap m g) ≤ g
• Filter.map_congr 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m₁ m₂ : α → β} {f : Filter α} (h : m₁ =ᶠ[f] m₂) : Filter.map m₁ f = Filter.map m₂ f
• Filter.seq_pure 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : Filter (α → β)) (a : α) : f.seq (pure a) = Filter.map (fun g => g a) f
• Filter.canLift 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Filter α) (Filter β) (Filter.map c) fun f => ∀ᶠ (x : α) in f, p x
• Filter.map_eq_bot_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} : Filter.map m f = ⊥ ↔ f = ⊥
• Filter.map_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : Filter β) (m : α → β) : Filter.map m (Filter.comap m f) = f ⊓ Filter.principal (Set.range m)
• Filter.map_comap_of_mem 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} (hf : Set.range m ∈ f) : Filter.map m (Filter.comap m f) = f
• Filter.map_inj 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (hm : Function.Injective m) : Filter.map m f = Filter.map m g ↔ f = g
• Filter.map_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {m' : β → γ} : Filter.map m' (Filter.map m f) = Filter.map (m' ∘ m) f
• Function.Semiconj.filter_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) : Function.Semiconj (Filter.map f) (Filter.map ga) (Filter.map gb)
• Set.InjOn.filter_map_Iic 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : Set.InjOn m s → Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s))
• Filter.filter_injOn_Iic_iff_injOn 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s)) ↔ Set.InjOn m s
• Filter.bind_map 📋 Mathlib.Order.Filter.Map
  {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : α → β) (f : Filter α) (g : β → Filter γ) : (Filter.map m f).bind g = f.bind (g ∘ m)
• Filter.image_mem_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α} (hs : s ∈ f) : m '' s ∈ Filter.map m f
• Filter.mem_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ m ⁻¹' t ∈ f
• Filter.neBot_inf_comap_iff_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : (F ⊓ Filter.comap f G).NeBot ↔ (Filter.map f F ⊓ G).NeBot
• Filter.neBot_inf_comap_iff_map' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : (Filter.comap f G ⊓ F).NeBot ↔ (G ⊓ Filter.map f F).NeBot
• Filter.map_compose 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : α → β} {m' : β → γ} : Filter.map m' ∘ Filter.map m = Filter.map (m' ∘ m)
• Filter.map_bind 📋 Mathlib.Order.Filter.Map
  {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : β → γ) (f : Filter α) (g : α → Filter β) : Filter.map m (f.bind g) = f.bind (Filter.map m ∘ g)
• Filter.map_iSup 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {m : α → β} {f : ι → Filter α} : Filter.map m (⨆ i, f i) = ⨆ i, Filter.map m (f i)
• Filter.map_sup 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {m : α → β} : Filter.map m (f₁ ⊔ f₂) = Filter.map m f₁ ⊔ Filter.map m f₂
• Filter.push_pull 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β) : Filter.map f (F ⊓ Filter.comap f G) = Filter.map f F ⊓ G
• Filter.push_pull' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter α) (G : Filter β) : Filter.map f (Filter.comap f G ⊓ F) = G ⊓ Filter.map f F
• Filter.eventuallyEq_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {f₁ f₂ : β → γ} : f₁ =ᶠ[Filter.map m f] f₂ ↔ f₁ ∘ m =ᶠ[f] f₂ ∘ m
• Set.LeftInvOn.filter_map_Iic 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {g : β → α} (hfg : Set.LeftInvOn g f s) : Set.LeftInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal s))
• Set.RightInvOn.filter_map_Iic 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {g : β → α} (hfg : Set.RightInvOn g f t) : Set.RightInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal t))
• Filter.image_mem_map_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {s : Set α} (hf : Function.Injective m) : m '' s ∈ Filter.map m f ↔ s ∈ f
• Filter.map_generate_le_generate_preimage_preimage 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (U : Set (Set β)) (f : β → α) : Filter.map f (Filter.generate U) ≤ Filter.generate ((fun x => f ⁻¹' x) ⁻¹' U)
• Filter.map_inf 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (h : Function.Injective m) : Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
• Filter.eventuallyLE_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} [LE γ] {f₁ f₂ : β → γ} : f₁ ≤ᶠ[Filter.map m f] f₂ ↔ f₁ ∘ m ≤ᶠ[f] f₂ ∘ m
• Filter.mem_map' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ {x | m x ∈ t} ∈ f
• GCongr.Filter.map_le_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m : α → β} {F G : Filter α} (h : F ≤ G) : Filter.map m F ≤ Filter.map m G
• Filter.comap_equiv_symm 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter α) : Filter.comap (⇑e.symm) f = Filter.map (⇑e) f
• Filter.map_eq_comap_of_inverse 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {n : β → α} (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) : Filter.map m f = Filter.comap n f
• Filter.map_equiv_symm 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter β) : Filter.map (⇑e.symm) f = Filter.comap (⇑e) f
• Filter.map_iInf_le 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β} : Filter.map m (iInf f) ≤ ⨅ i, Filter.map m (f i)
• Filter.map_le_iff_le_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {m : α → β} : Filter.map m f ≤ g ↔ f ≤ Filter.comap m g
• Filter.map_inf_le 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} : Filter.map m (f ⊓ g) ≤ Filter.map m f ⊓ Filter.map m g
• Set.SurjOn.filter_map_Iic 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.SurjOn m s t → Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))
• Filter.map_surjOn_Iic_iff_surjOn 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.SurjOn m s t
• Filter.map_le_map_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} (hm : Function.Injective m) : Filter.map m f ≤ Filter.map m g ↔ f ≤ g
• Filter.prod_map_seq_comm 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) : (Filter.map Prod.mk f).seq g = (Filter.map (fun b a => (a, b)) g).seq f
• Filter.mem_map_iff_exists_image 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ ∃ s ∈ f, m '' s ⊆ t
• Filter.le_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β} (h : ∀ s ∈ f, m '' s ∈ g) : g ≤ Filter.map m f
• Filter.le_map_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β} : g ≤ Filter.map m f ↔ ∀ s ∈ f, m '' s ∈ g
• Filter.map_comm 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ) (F : Filter α) : Filter.map ψ (Filter.map φ F) = Filter.map ρ (Filter.map θ F)
• Filter.seq_assoc 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)) : h.seq (g.seq x) = ((Filter.map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x
• Filter.map_eq_map_iff_of_injOn 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {s : Set α} (hsf : s ∈ f) (hsg : s ∈ g) (hm : Set.InjOn m s) : Filter.map m f = Filter.map m g ↔ f = g
• Filter.map_surjOn_Iic_iff_le_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.SurjOn (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ G ≤ Filter.map m F
• Filter.principal_eq_map_coe_top 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} (s : Set α) : Filter.principal s = Filter.map Subtype.val ⊤
• Filter.map_iInf_eq 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β} (hf : Directed (fun x1 x2 => x1 ≥ x2) f) [Nonempty ι] : Filter.map m (iInf f) = ⨅ i, Filter.map m (f i)
• Filter.disjoint_of_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_6} {β : Type u_7} {F G : Filter α} {f : α → β} (h : Disjoint (Filter.map f F) (Filter.map f G)) : Disjoint F G
• Filter.map_inf' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g) (h : Set.InjOn m t) : Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
• Filter.disjoint_comap_iff_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : Disjoint F (Filter.comap f G) ↔ Disjoint (Filter.map f F) G
• Filter.disjoint_comap_iff_map' 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β} : Disjoint (Filter.comap f G) F ↔ Disjoint G (Filter.map f F)
• Filter.map_comap_setCoe_val 📋 Mathlib.Order.Filter.Map
  {β : Type u_2} (f : Filter β) (s : Set β) : Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s
• Filter.subtype_coe_map_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} (s : Set α) (f : Filter α) : Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s
• Filter.disjoint_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {m : α → β} (hm : Function.Injective m) {f₁ f₂ : Filter α} : Disjoint (Filter.map m f₁) (Filter.map m f₂) ↔ Disjoint f₁ f₂
• Filter.map_le_map_iff_of_injOn 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {l₁ l₂ : Filter α} {f : α → β} {s : Set α} (h₁ : s ∈ l₁) (h₂ : s ∈ l₂) (hinj : Set.InjOn f s) : Filter.map f l₁ ≤ Filter.map f l₂ ↔ l₁ ≤ l₂
• Filter.mem_map_seq_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {m : α → β → γ} {s : Set γ} : s ∈ (Filter.map m f).seq g ↔ ∃ t u, t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s
• Filter.map_biInf_eq 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop} (h : DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x}) (ne : ∃ i, p i) : Filter.map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), Filter.map m (f i)
• Filter.map_swap4_eq_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter ((α × β) × γ × δ)} : Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f
• Filter.Tendsto.eq_1 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Filter.Tendsto f l₁ l₂ = (Filter.map f l₁ ≤ l₂)
• Filter.HasAntitoneBasis.map 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι'' → Set α} (hf : l.HasAntitoneBasis s) (m : α → β) : (Filter.map m l).HasAntitoneBasis fun x => m '' s x
• Filter.HasBasis.map 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β) (hl : l.HasBasis p s) : (Filter.map f l).HasBasis p fun i => f '' s i
• Filter.map_sigma_mk_comap 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {π : α → Type u_6} {π' : β → Type u_7} {f : α → β} (hf : Function.Injective f) (g : (a : α) → π a → π' (f a)) (a : α) (l : Filter (π' (f a))) : Filter.map (Sigma.mk a) (Filter.comap (g a) l) = Filter.comap (Sigma.map f g) (Filter.map (Sigma.mk (f a)) l)
• Filter.tendsto_map 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} : Filter.Tendsto f x (Filter.map f x)
• Filter.tendsto_map' 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} : Filter.Tendsto (f ∘ g) x y → Filter.Tendsto f (Filter.map g x) y
• Filter.tendsto_map'_iff 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} : Filter.Tendsto f (Filter.map g x) y ↔ Filter.Tendsto (f ∘ g) x y
• Filter.map_inf_principal_preimage 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} {l : Filter α} : Filter.map f (l ⊓ Filter.principal (f ⁻¹' s)) = Filter.map f l ⊓ Filter.principal s
• Filter.Tendsto.map_mapsTo_Iic 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Filter.Tendsto m F G → Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G)
• Filter.map_eq_of_inverse 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id) (hφ : Filter.Tendsto φ f g) (hψ : Filter.Tendsto ψ g f) : Filter.map φ f = g
• Filter.map_mapsTo_Iic_iff_tendsto 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ Filter.Tendsto m F G
• Filter.le_map_of_right_inverse 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β} (h₁ : mab ∘ mba =ᶠ[g] id) (h₂ : Filter.Tendsto mba g f) : g ≤ Filter.map mab f
• Set.MapsTo.filter_map_Iic 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.MapsTo m s t → Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))
• Filter.map_mapsTo_Iic_iff_mapsTo 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.MapsTo m s t
• Nat.map_cast_int_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  : Filter.map Nat.cast Filter.atTop = Filter.atTop
• Filter.map_add_atTop_eq_nat 📋 Mathlib.Order.Filter.AtTopBot.Basic
  (k : ℕ) : Filter.map (fun a => a + k) Filter.atTop = Filter.atTop
• Filter.map_sub_atTop_eq_nat 📋 Mathlib.Order.Filter.AtTopBot.Basic
  (k : ℕ) : Filter.map (fun a => a - k) Filter.atTop = Filter.atTop
• Filter.map_div_atTop_eq_nat 📋 Mathlib.Order.Filter.AtTopBot.Basic
  (k : ℕ) (hk : 0 < k) : Filter.map (fun a => a / k) Filter.atTop = Filter.atTop
• Filter.map_atBot_eq 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] [Nonempty α] {f : α → β} : Filter.map f Filter.atBot = ⨅ a, Filter.principal (f '' {a' | a' ≤ a})
• Filter.map_atTop_eq 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] [Nonempty α] {f : α → β} : Filter.map f Filter.atTop = ⨅ a, Filter.principal (f '' {a' | a ≤ a'})
• Filter.inf_map_atBot_neBot_iff 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] {F : Filter β} {u : α → β} : (F ⊓ Filter.map u Filter.atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U
• Filter.inf_map_atTop_neBot_iff 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] {F : Filter β} {u : α → β} [Nonempty α] : (F ⊓ Filter.map u Filter.atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
• Filter.map_val_Ici_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] (a : α) : Filter.map Subtype.val Filter.atTop = Filter.atTop
• Filter.map_val_Iic_atBot 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] (a : α) : Filter.map Subtype.val Filter.atBot = Filter.atBot
• Filter.map_val_atTop_of_Ici_subset 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] {a : α} {s : Set α} (h : Set.Ici a ⊆ s) : Filter.map Subtype.val Filter.atTop = Filter.atTop
• Filter.map_atBot_eq_of_gc_preorder 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] [Preorder β] [IsDirected β fun x1 x2 => x1 ≥ x2] {f : α → β} (hf : Monotone f) (b : β) (hgi : ∀ c ≤ b, ∃ x, f x = c ∧ ∀ (a : α), c ≤ f a ↔ x ≤ a) : Filter.map f Filter.atBot = Filter.atBot
• Filter.map_atTop_eq_of_gc_preorder 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] [Preorder β] [IsDirected β fun x1 x2 => x1 ≤ x2] {f : α → β} (hf : Monotone f) (b : β) (hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x) : Filter.map f Filter.atTop = Filter.atTop
• Filter.map_val_Iio_atBot 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] [NoMinOrder α] (a : α) : Filter.map Subtype.val Filter.atBot = Filter.atBot
• Filter.map_val_Ioi_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] [NoMaxOrder α] (a : α) : Filter.map Subtype.val Filter.atTop = Filter.atTop
• Filter.map_atBot_eq_of_gc 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≥ x2] [PartialOrder β] [IsDirected β fun x1 x2 => x1 ≥ x2] {f : α → β} (g : β → α) (b' : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) : Filter.map f Filter.atBot = Filter.atBot
• Filter.map_atTop_eq_of_gc 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun x1 x2 => x1 ≤ x2] [PartialOrder β] [IsDirected β fun x1 x2 => x1 ≤ x2] {f : α → β} (g : β → α) (b : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ c ≥ b, f a ≤ c ↔ a ≤ g c) (hgi : ∀ c ≥ b, c ≤ f (g c)) : Filter.map f Filter.atTop = Filter.atTop
• Filter.map_fst_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [g.NeBot] : Filter.map Prod.fst (f ×ˢ g) = f
• Filter.map_snd_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [f.NeBot] : Filter.map Prod.snd (f ×ˢ g) = g
• Filter.pure_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {a : α} {f : Filter β} : pure a ×ˢ f = Filter.map (Prod.mk a) f
• Filter.prod_pure 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {b : β} : f ×ˢ pure b = Filter.map (fun a => (a, b)) f
• Filter.prod_eq 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : f ×ˢ g = (Filter.map Prod.mk f).seq g
• Filter.map_pure_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (B : Filter β) : Filter.map (Function.uncurry f) (pure a ×ˢ B) = Filter.map (f a) B
• Filter.map_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × β → γ) (f : Filter α) (g : Filter β) : Filter.map m (f ×ˢ g) = (Filter.map (fun a b => m (a, b)) f).seq g
• Filter.le_prod_map_fst_snd 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} : f ≤ Filter.map Prod.fst f ×ˢ Filter.map Prod.snd f
• Filter.prod_comm 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : f ×ˢ g = Filter.map (fun p => (p.2, p.1)) (g ×ˢ f)
• Filter.prod_map_left 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (F : Filter α) (G : Filter γ) : Filter.map f F ×ˢ G = Filter.map (Prod.map f id) (F ×ˢ G)
• Filter.prod_map_right 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (F : Filter α) (G : Filter β) : F ×ˢ Filter.map f G = Filter.map (Prod.map id f) (F ×ˢ G)
• Filter.map_prodMap_coprod_le 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} : Filter.map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (Filter.map m₁ f₁).coprod (Filter.map m₂ f₂)
• Filter.map_prod_map_coprod_le 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} : Filter.map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (Filter.map m₁ f₁).coprod (Filter.map m₂ f₂)
• Filter.prod_map_map_eq' 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) : Filter.map f F ×ˢ Filter.map g G = Filter.map (Prod.map f g) (F ×ˢ G)
• Filter.map_prodMap_const_id_principal_coprod_principal 📋 Mathlib.Order.Filter.Prod
  {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) : Filter.map (Prod.map (fun x => b) id) ((Filter.principal {a}).coprod (Filter.principal {i})) = Filter.principal ({b} ×ˢ Set.univ)
• Filter.map_prod_map_const_id_principal_coprod_principal 📋 Mathlib.Order.Filter.Prod
  {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) : Filter.map (Prod.map (fun x => b) id) ((Filter.principal {a}).coprod (Filter.principal {i})) = Filter.principal ({b} ×ˢ Set.univ)
• Filter.prod_map_map_eq 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} : Filter.map m₁ f₁ ×ˢ Filter.map m₂ f₂ = Filter.map (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
• Filter.map_const_principal_coprod_map_id_principal 📋 Mathlib.Order.Filter.Prod
  {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) : (Filter.map (fun x => b) (Filter.principal {a})).coprod (Filter.map id (Filter.principal {i})) = Filter.principal ({b} ×ˢ Set.univ ∪ Set.univ ×ˢ {i})
• Filter.prod_assoc 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) : Filter.map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
• Filter.prod_assoc_symm 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ) : Filter.map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
• Filter.map_swap4_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : Filter α} {g : Filter β} {h : Filter γ} {k : Filter δ} : Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
• Filter.lift'_map_le 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β} : (Filter.map m f).lift' g ≤ f.lift' (g ∘ Set.image m)
• Filter.lift_map_le 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Filter γ} {m : α → β} : (Filter.map m f).lift g ≤ f.lift (g ∘ Set.image m)
• Filter.map_lift_eq 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {m : β → γ} (hg : Monotone g) : Filter.map m (f.lift g) = f.lift (Filter.map m ∘ g)
• Filter.map_lift_eq2 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Filter γ} {m : α → β} (hg : Monotone g) : (Filter.map m f).lift g = f.lift (g ∘ Set.image m)
• Filter.map_lift'_eq 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : β → γ} (hh : Monotone h) : Filter.map m (f.lift' h) = f.lift' (Set.image m ∘ h)
• Filter.map_lift'_eq2 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β} (hg : Monotone g) : (Filter.map m f).lift' g = f.lift' (g ∘ Set.image m)
• Filter.map.isCountablyGenerated 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} {β : Type u_2} (l : Filter α) [l.IsCountablyGenerated] (f : α → β) : (Filter.map f l).IsCountablyGenerated
• Filter.map_eval_pi 📋 Mathlib.Order.Filter.Pi
  {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).NeBot] (i : ι) : Filter.map (Function.eval i) (Filter.pi f) = f i
• Filter.map_pi_map_coprodᵢ_le 📋 Mathlib.Order.Filter.Pi
  {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : ι → Type u_3} {m : (i : ι) → α i → β i} : Filter.map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => Filter.map (m i) (f i)
• Function.Surjective.le_map_cofinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Function.Surjective f) : Filter.cofinite ≤ Filter.map f Filter.cofinite
• Filter.map_piMap_pi_finite 📋 Mathlib.Order.Filter.Cofinite
  {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [Finite ι] (f : (i : ι) → α i → β i) (l : (i : ι) → Filter (α i)) : Filter.map (Pi.map f) (Filter.pi l) = Filter.pi fun i => Filter.map (f i) (l i)
• Filter.map_piMap_pi 📋 Mathlib.Order.Filter.Cofinite
  {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {f : (i : ι) → α i → β i} (hf : ∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i)) (l : (i : ι) → Filter (α i)) : Filter.map (Pi.map f) (Filter.pi l) = Filter.pi fun i => Filter.map (f i) (l i)
• limUnder.eq_1 📋 Mathlib.Topology.Basic
  {X : Type u_1} [TopologicalSpace X] {α : Type u_3} [Nonempty X] (f : Filter α) (g : α → X) : limUnder f g = lim (Filter.map g f)
• map_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : X → α} : Filter.map f (nhds x) = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)
• MapClusterPt.clusterPt 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u → ClusterPt x (Filter.map u F)
• mapClusterPt_def 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)
• MapClusterPt.eq_1 📋 Mathlib.Topology.ClusterPt
  {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ι → X) : MapClusterPt x F u = ClusterPt x (Filter.map u F)
• mapClusterPt_comp 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {β : Type u_2} {F : Filter α} {x : X} {φ : α → β} {u : β → X} : MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u
• MapClusterPt.tendsto_comp' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u)
• coinduced_nhdsAdjoint 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} (f : α → β) (a : α) (l : Filter α) : TopologicalSpace.coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (Filter.map f l)
• map_nhds_induced_eq 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} (a : α) : Filter.map f (nhds a) = nhdsWithin (f a) (Set.range f)
• map_nhds_induced_of_surjective 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [T : TopologicalSpace α] {f : β → α} (hf : Function.Surjective f) (a : β) : Filter.map f (nhds a) = nhds (f a)
• map_nhds_induced_of_mem 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} (h : Set.range f ∈ nhds (f a)) : Filter.map f (nhds a) = nhds (f a)
• Topology.IsOpenEmbedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) (x : X) : Filter.map f (nhds x) = nhds (f x)
• Topology.IsEmbedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
• Topology.IsInducing.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
• Topology.IsEmbedding.Embedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
• IsOpenMap.nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) : nhds (f x) ≤ Filter.map f (nhds x)
• IsOpenMap.of_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)) : IsOpenMap f
• isOpenMap_iff_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap f ↔ ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
• IsClosedMap.lift'_closure_map_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) : (Filter.map f F).lift' closure = Filter.map f (F.lift' closure)
• Topology.IsEmbedding.map_nhds_of_mem 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) (h : Set.range f ∈ nhds (f x)) : Filter.map f (nhds x) = nhds (f x)
• Topology.IsInducing.map_nhds_of_mem 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) (x : X) (h : Set.range f ∈ nhds (f x)) : Filter.map f (nhds x) = nhds (f x)
• Topology.IsEmbedding.Embedding.map_nhds_of_mem 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) (h : Set.range f ∈ nhds (f x)) : Filter.map f (nhds x) = nhds (f x)
• Homeomorph.map_nhds_eq 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h) (nhds x) = nhds (h x)
• Homeomorph.symm_map_nhds_eq 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h.symm) (nhds (h x)) = nhds x
• map_fst_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhds x) = nhds x.1
• map_snd_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.snd (nhds x) = nhds x.2
• nhds_inl 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : nhds (Sum.inl x) = Filter.map Sum.inl (nhds x)
• nhds_inr 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) : nhds (Sum.inr y) = Filter.map Sum.inr (nhds y)
• nhds_swap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) : nhds (x, y) = Filter.map Prod.swap (nhds (y, x))
• map_fst_nhdsWithin 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1
• map_snd_nhdsWithin 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2
• Sigma.nhds_mk 📋 Mathlib.Topology.Constructions
  {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] (i : ι) (x : σ i) : nhds ⟨i, x⟩ = Filter.map (Sigma.mk i) (nhds x)
• map_nhds_subtype_coe_eq_nhds 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {p : X → Prop} {x : X} (hx : p x) (h : ∀ᶠ (x : X) in nhds x, p x) : Filter.map Subtype.val (nhds ⟨x, hx⟩) = nhds x
• nhds_ofAdd 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : X) : nhds (Multiplicative.ofAdd x) = Filter.map (⇑Multiplicative.ofAdd) (nhds x)
• nhds_ofMul 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : X) : nhds (Additive.ofMul x) = Filter.map (⇑Additive.ofMul) (nhds x)
• nhds_toDual 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : X) : nhds (OrderDual.toDual x) = Filter.map (⇑OrderDual.toDual) (nhds x)
• nhds_ofDual 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : X) : nhds (OrderDual.ofDual x) = Filter.map (⇑OrderDual.ofDual) (nhds x)
• nhds_toAdd 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : Multiplicative X) : nhds (Multiplicative.toAdd x) = Filter.map (⇑Multiplicative.toAdd) (nhds x)
• nhds_toMul 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (x : Additive X) : nhds (Additive.toMul x) = Filter.map (⇑Additive.toMul) (nhds x)
• Sigma.nhds_eq 📋 Mathlib.Topology.Constructions
  {ι : Type u_5} {σ : ι → Type u_7} [(i : ι) → TopologicalSpace (σ i)] (x : Sigma σ) : nhds x = Filter.map (Sigma.mk x.fst) (nhds x.snd)
• map_nhds_subtype_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set X} (x : ↑s) : Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
• Embedding.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsEmbedding f) (s : Set α) (x : α) : Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
• Topology.IsEmbedding.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsEmbedding f) (s : Set α) (x : α) : Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
• Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsOpenEmbedding f) (s : Set β) (x : α) : Filter.map f (nhdsWithin x (f ⁻¹' s)) = nhdsWithin (f x) s
• Function.LeftInverse.map_nhds_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (Set.range g) (g x)) (hg : ContinuousAt g x) : Filter.map g (nhds x) = nhdsWithin (g x) (Set.range g)
• Set.LeftInvOn.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} {s : Set β} (h : Set.LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65