Mathlib Map

Theorems · Theorem · general topology

Filter.map_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
Defined in
Mathlib.Order.Filter.Map
Cited by
80 results in Mathlib
Foundations
Depth 12 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Filter.tendsto_comap_iff · cited by 55Filter.tendsto_comap_iffFilter.tendsto_map'_iff · cited by 50Filter.tendsto_map'_iffFilter.prod_pure · cited by 30Filter.prod_pureIsUniformInducing.uniformContinuous_iff · cited by 17IsUniformInducing.uniform…Filter.map₂_pure_right · cited by 9Filter.map₂_pure_rightFilter.map₂_pure_left · cited by 8Filter.map₂_pure_leftOpenPartialHomeomorph.map_extend_nhds · cited by 6OpenPartialHomeomorph.map…Filter.map₂_swap · cited by 6Filter.map₂_swapFilter.map_snd_prod · cited by 5Filter.map_snd_prodAffineSpace.asymptoticNhds_vadd_pure · cited by 5AffineSpace.asymptoticNhd…Filter.map₂_map_left · cited by 5Filter.map₂_map_leftOpenPartialHomeomorph.map_extend_symm_nhdsWithin · cited by 4OpenPartialHomeomorph.map…Filter.map_equiv_symm · cited by 4Filter.map_equiv_symmFilter.map_map₂ · cited by 4Filter.map_map₂AffineSpace.asymptoticNhds_eq_smul · cited by 4AffineSpace.asymptoticNhd…Filter · cited by 8121FilterFilter.map · cited by 819Filter.mapFilter.map_compose · cited by 3Filter.map_composeFilter.map_mapCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by80

Results whose statement or proof uses this declaration.