Theorems · Theorem · functional analysis
Filter.comap_mul_right_cobounded
∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [NormMulClass α] {a : α},
a ≠ 0 → Filter.comap (fun x => x * a) (Bornology.cobounded α) = Bornology.cobounded α- Defined in
- Mathlib.Analysis.Normed.Ring.Lemmas
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- Filter.comapstatement · cited by 546
- NonUnitalNormedRingstatement and proof · cited by 231
- Bornology.coboundedstatement · cited by 162
- NormMulClassstatement and proof · cited by 66
- Dilation.comap_coboundedproof · cited by 3
- Dilation.mulRightproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.