Theorems · Theorem · functional analysis
Absorbs.exists_pos
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
Absorbs 𝕜 A B → ∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A- Defined in
- Mathlib.Analysis.LocallyConvex.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedRingSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Realstatement and proof · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- Set.preimageproof · cited by 4,946
- Set.Iciproof · cited by 1,070
- LT.lt.trans_leproof · cited by 678
- Set.smulSetstatement · cited by 608
- SeminormedRingstatement and proof · cited by 446
- one_posproof · cited by 102
- Absorbsstatement and proof · cited by 59
- Filter.HasBasis.eventually_iffproof · cited by 38
- Filter.HasBasis.cobounded_of_normproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- NormedSpace.isVonNBounded_iffproof · cited by 9
- IsCompactOperator.image_subset_compact_of_isVonNBoundedproof · cited by 4
- Absorbent.gauge_set_nonemptyproof · cited by 2
- WithSeminorms.isVonNBounded_iff_finset_seminorm_boundedproof · cited by 2
- comap_gauge_nhds_zero_leproof · cited by 2
- le_gauge_of_notMemproof · cited by 1
- NormedSpace.isBounded_iff_subset_smul_ballproof · cited by 1
- IsCompactOperator.continuousproof · cited by 0