Mathlib Map

Theorems · Theorem · general topology

absorbent_iff_forall_absorbs_singleton

∀ {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
1 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.

Seminorm.absorbent_ball_zero · cited by 4Seminorm.absorbent_ball_z…Set · cited by 53352SetBornology · cited by 188BornologyAbsorbent · cited by 60AbsorbentAbsorbs · cited by 59Absorbsabsorbent_iff_forall_absorbs_…CITED 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 · cited by 60
  • Absorbsstatement · cited by 59

Cited by1

Results whose statement or proof uses this declaration.