Mathlib Map

Theorems · Theorem · general topology

Absorbent.absorbs

∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α},
  Absorbent M s → ∀ {x : α}, Absorbs M s {x}
Defined in
Mathlib.Topology.Bornology.Absorbs
Cited by
3 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
BornologySMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Bornology.isVonNBounded_singleton · cited by 2Bornology.isVonNBounded_s…separate_convex_open_set · cited by 2separate_convex_open_setAbsorbent.absorbs_finite · cited by 1Absorbent.absorbs_finiteSet · cited by 53352SetBornology · cited by 188BornologyAbsorbent · cited by 60AbsorbentAbsorbs · cited by 59AbsorbsAbsorbent.absorbsCITED BYCITES

Cites4

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
  • Bornologystatement and proof · cited by 188
  • Absorbentstatement and proof · cited by 60
  • Absorbsstatement · cited by 59

Cited by3

Results whose statement or proof uses this declaration.