Theorems · Theorem · general topology
Absorbs.mono_right
∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t₁ t₂ : Set α},
Absorbs M s t₁ → t₂ ⊆ t₁ → Absorbs M s t₂- Defined in
- Mathlib.Topology.Bornology.Absorbs
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- LE.le.transproof · cited by 3,151
- Filter.Eventually.monoproof · cited by 646
- Bornologystatement and proof · cited by 188
- Absorbsstatement and proof · cited by 59
Cited by6
Results whose statement or proof uses this declaration.
- Seminorm.absorbent_ball_zeroproof · cited by 4
- TotallyBounded.isVonNBoundedproof · cited by 4
- NormedSpace.isVonNBounded_of_isBoundedproof · cited by 4
- Bornology.IsVonNBounded.subsetproof · cited by 3
- WithSeminorms.isVonNBounded_iff_finset_seminorm_boundedproof · cited by 2
- Absorbs.monoproof · cited by 0