surjOn_logb' — Mathlib

English

Let b > 1 with b ≠ 1. Then the restriction of log_b to the negative reals is surjective onto ℝ.

Русский

Пусть b > 1. Тогда ограничение log_b на отрицательных вещественных числах отображает ℝ сюръективно на ℝ.

LaTeX

$$$0 < b \land b \neq 1 \Rightarrow \operatorname{SurjOn}(\log_b b) (\mathbb{I\!I}^-) \; ?$$$

Lean4

theorem surjOn_logb' : SurjOn (logb b) (Iio 0) univ := by
  intro x _
  use -b ^ x
  constructor
  · simp only [Right.neg_neg_iff, Set.mem_Iio]
    apply rpow_pos_of_pos b_pos
  · rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

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