Theorems · Theorem · general topology
Filter.Tendsto.le_comap
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ → l₁ ≤ Filter.comap f l₂Alias of the forward direction of Filter.tendsto_iff_comap.
- Defined in
- Mathlib.Order.Filter.Tendsto
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.Tendstostatement · cited by 3,814
- Filter.comapstatement · cited by 546
- Filter.tendsto_iff_comapproof · cited by 19
Cited by28
Results whose statement or proof uses this declaration.
- Topology.IsOpenEmbedding.of_continuous_injective_isOpenMapproof · cited by 13
- AntilipschitzWith.isUniformInducingproof · cited by 8
- Filter.Tendsto.eventually_forall_ge_atTopproof · cited by 7
- IsUniformInducing.of_compproof · cited by 5
- Filter.Tendsto.disjointproof · cited by 4
- Filter.comap_embedding_atTopproof · cited by 4
- Dilation.comap_coboundedproof · cited by 3
- Filter.comap_embedding_atBotproof · cited by 3
- IsDiscrete.preimage'proof · cited by 2
- Filter.comap_abs_atTopproof · cited by 2
- Filter.Tendsto.countable_compl_preimage_kerproof · cited by 2
- uniformity_le_symmproof · cited by 2