Theorems · Definition · general topology
Absorbent
(M : Type u_1) → {α : Type u_2} → [Bornology M] → [SMul M α] → Set α → PropA set is absorbent if it absorbs every singleton.
- Defined in
- Mathlib.Topology.Bornology.Absorbs
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by62
Results whose statement or proof uses this declaration.
- absorbent_nhds_zerostatement · cited by 16
- Absorbent.monostatement and proof · cited by 7
- exists_lt_of_gauge_ltstatement and proof · cited by 6
- gaugeSeminormstatement and proof · cited by 6
- setOfPred_gauge_lt_one_subset_selfstatement and proof · cited by 5
- gauge_add_lestatement and proof · cited by 4
- gauge_monostatement and proof · cited by 4
- gauge_posstatement and proof · cited by 4
- Seminorm.absorbent_ball_zerostatement · cited by 4
- mem_closure_of_gauge_le_onestatement and proof · cited by 3
- absorbent_ball_zerostatement and proof · cited by 3
- Absorbent.absorbsstatement and proof · cited by 3