Theorems · Theorem · general topology
MapClusterPt.mono
∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {G : Filter α},
MapClusterPt x F u → F ≤ G → MapClusterPt x G u- Defined in
- Mathlib.Topology.ClusterPt
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- MapClusterPtstatement and proof · cited by 78
- Filter.map_monoproof · cited by 63
- ClusterPt.monoproof · cited by 30
- MapClusterPt.clusterPtproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- mapClusterPt_leftLimproof · cited by 3
- tendsto_rightLim_atTop_of_tendstoproof · cited by 2
- tendsto_leftLim_atTop_of_tendstoproof · cited by 2
- eVariationOn.eVariationOn_leftLim_leproof · cited by 1
- eVariationOn.eVariationOn_rightLim_leproof · cited by 1
- MapClusterPt.prodMapproof · cited by 0