exp_lt_exp

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#WithZero.exp_lt_exp

English

Exponential map is strictly order-preserving: exp a < exp b iff a < b.

Русский

Экспоненциальная карта строго сохраняет порядок: exp a < exp b тогда и только тогда, когда a < b.

LaTeX

$$$\exp a < \exp b \iff a < b$$$

Lean4

@[simp]
theorem exp_lt_exp : exp a < exp b ↔ a < b := by simp [exp]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru