Theorems · Theorem · general topology
Filter.map_equiv_symm
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter β), Filter.map (⇑e.symm) f = Filter.comap (⇑e) f- Defined in
- Mathlib.Order.Filter.Map
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement and proof · cited by 8,337
- Filterstatement and proof · cited by 8,121
- Equiv.symmstatement and proof · cited by 3,681
- Filter.mapstatement and proof · cited by 819
- Filter.comapstatement and proof · cited by 546
- Equiv.injectiveproof · cited by 464
- Equiv.surjectiveproof · cited by 198
- Filter.map_mapproof · cited by 80
- Equiv.self_comp_symmproof · cited by 28
- Filter.map_idproof · cited by 22
- Filter.map_comap_of_surjectiveproof · cited by 11
Cited by4
Results whose statement or proof uses this declaration.
- Filter.map_eq_comap_of_inverseproof · cited by 5
- Equiv.isUniformEmbeddingproof · cited by 2
- Filter.prod_assoc_symmproof · cited by 1
- AbsoluteValue.IsEquiv.isEmbedding_equivWithAbsproof · cited by 1