Theorems · Theorem · commutative algebra
seminormFromBounded_isNonarchimedean
∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → IsNonarchimedean f → IsNonarchimedean (seminormFromBounded' f)If f : R → ℝ is a nonnegative, multiplicatively bounded, nonarchimedean function, then
seminormFromBounded' f is nonarchimedean.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- CommRingstatement and proof · cited by 17,173
- add_mulproof · cited by 363
- div_zeroproof · cited by 251
- lt_of_le_of_ne'proof · cited by 149
- IsNonarchimedeanstatement and proof · cited by 77
- ciSup_leproof · cited by 56
- le_max_iffproof · cited by 26
- le_ciSup_of_leproof · cited by 22
- div_le_div_iff_of_pos_rightproof · cited by 20
- seminormFromBounded'statement · cited by 17
- seminormFromBounded_bddAbove_rangeproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensionalproof · cited by 5