English
A ring homomorphism f: α → β is bounded with respect to nα and nβ if there exists C > 0 with nβ(f x) ≤ C nα(x) for all x.
Русский
Гомоморф кольцa f: α → β ограничен относительно функций nα и nβ, если существует C > 0 с nβ(f(x)) ≤ C nα(x) для всех x.
LaTeX
$$$\exists C \in \mathbb{R},\ 0 < C \wedge \forall x:\alpha,\ n_\beta(f(x)) \le C \cdot n_\alpha(x)$$$
Lean4
/-- A ring homomorphism `f : α →+* β` is bounded with respect to the functions `nα : α → ℝ` and
`nβ : β → ℝ` if there exists a positive constant `C` such that for all `x` in `α`,
`nβ (f x) ≤ C * nα x`. -/
def IsBoundedWrt {α : Type*} [Ring α] {β : Type*} [Ring β] (nα : α → ℝ) (nβ : β → ℝ) (f : α →+* β) : Prop :=
∃ C : ℝ, 0 < C ∧ ∀ x : α, nβ (f x) ≤ C * nα x
