Theorems · Theorem · general topology
Filter.Eventually.comap
∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {p : β → Prop},
(∀ᶠ (b : β) in g, p b) → ∀ (f : α → β), ∀ᶠ (a : α) in Filter.comap f g, p (f a)- Defined in
- Mathlib.Order.Filter.Map
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 60 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.Eventuallystatement and proof · cited by 3,134
- Filter.comapstatement · cited by 546
- Filter.preimage_mem_comapproof · cited by 23
Cited by10
Results whose statement or proof uses this declaration.
- Filter.Tendsto.eventually_forall_ge_atTopproof · cited by 7
- IsPreconnected.intermediate_value₂_eventually₁proof · cited by 4
- IsPreconnected.intermediate_value₂_eventually₂proof · cited by 4
- eventually_nhdsGT_zero_mul_leftproof · cited by 2
- Filter.Eventually.intCast_atBotproof · cited by 0
- Filter.Eventually.intCast_atTopproof · cited by 0
- Filter.Tendsto.eventually_forall_le_atBotproof · cited by 0
- Filter.EventuallyEq.comp_comapproof · cited by 0
- Filter.Eventually.ratCast_atBotproof · cited by 0
- Filter.Eventually.ratCast_atTopproof · cited by 0