Mathlib Map

Theorems · Theorem · general topology

Absorbs.neg_neg

∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
  [inst_3 : Bornology M] {s t : Set E}, Absorbs M s t → Absorbs M (-s) (-t)

Alias of the reverse direction of absorbs_neg_neg.

Defined in
Mathlib.Topology.Bornology.Absorbs
Cited by
2 results in Mathlib
Foundations
Depth 29 from the axioms · uses propext, Quot.sound
Assumes
MonoidAddGroupDistribMulActionBornology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Bornology.IsVonNBounded.neg · cited by 2IsVonNBounded.negAbsorbs.sub · cited by 0Absorbs.subSet · cited by 53352SetAddGroup · cited by 4410AddGroupMonoid · cited by 3887MonoidDistribMulAction · cited by 584DistribMulActionBornology · cited by 188BornologySet.neg · cited by 168Set.negAbsorbs · cited by 59Absorbsabsorbs_neg_neg · cited by 2absorbs_neg_negAbsorbs.neg_negCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.