Theorems · Theorem · general topology
Filter.comap_lift_eq2
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Filter γ},
Monotone g → (Filter.comap m f).lift g = f.lift (g ∘ Set.preimage m)- Defined in
- Mathlib.Order.Filter.Lift
- Cited by
- 3 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.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Set.preimagestatement and proof · cited by 4,946
- le_antisymmproof · cited by 2,068
- Monotonestatement and proof · cited by 1,397
- Filter.comapstatement and proof · cited by 546
- Set.Subset.rflproof · cited by 255
- le_iInf₂proof · cited by 67
- Filter.liftstatement and proof · cited by 45
- iInf₂_leproof · cited by 45
- iInf₂_le_of_leproof · cited by 29
Cited by3
Results whose statement or proof uses this declaration.
- Filter.comap_lift'_eq2proof · cited by 2
- lift_nhds_leftproof · cited by 0
- lift_nhds_rightproof · cited by 0