Theorems · Theorem · general topology
Filter.comap_comap
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : γ → β} {n : β → α},
Filter.comap m (Filter.comap n f) = Filter.comap (n ∘ m) f- Defined in
- Mathlib.Order.Filter.Map
- Cited by
- 69 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Set.imageproof · cited by 5,609
- Compl.complproof · cited by 2,925
- Filter.comapstatement · cited by 546
- Set.image_congrproof · cited by 533
- Set.image_imageproof · cited by 140
- Filter.coextproof · cited by 3
Cited by69
Results whose statement or proof uses this declaration.
- IsUniformInducing.compproof · cited by 11
- IsUniformInducing.of_comp_iffproof · cited by 10
- IsUniformInducing.of_compproof · cited by 5
- Filter.prod_comap_comap_eqproof · cited by 5
- LinearMap.withSeminorms_inducedproof · cited by 5
- uniformity_prod_eq_comap_prodproof · cited by 5
- Complex.comap_exp_nhds_zeroproof · cited by 4
- Filter.Tendsto.of_tendsto_compproof · cited by 4
- PhragmenLindelof.quadrant_Iproof · cited by 4
- Topology.IsEmbedding.toPullbackDiagproof · cited by 4
- uniformity_eq_comap_nhds_zero_swappedproof · cited by 4
- IsDenseEmbedding.subtypeproof · cited by 3