logb_surjective — Mathlib

English

Assume 0 < b and b ≠ 1. Then the map x ↦ log_b x is surjective from ℝ to ℝ, i.e., for every t ∈ ℝ there exists x ∈ ℝ with log_b x = t.

Русский

Пусть 0 < b и b ≠ 1. Тогда отображение x ↦ log_b x отображает ℝ на ℝ сюръективно, то есть для каждого t ∈ ℝ существует x ∈ ℝ such that log_b x = t.

LaTeX

$$$0 < b \land b \neq 1 \Rightarrow \forall t \in \mathbb{R}, \exists x \in \mathbb{R}: \log_b x = t.$$$

Lean4

theorem logb_surjective : Surjective (logb b) := fun x => ⟨b ^ x, logb_rpow b_pos b_ne_one⟩

Похожие утверждения