inv_lt_one_of_one_lt₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#inv_lt_one_of_one_lt₀

English

1 < inv a iff 0 < a ∧ a < 1.

Русский

1 < inv a тогда и только тогда, когда 0 < a и a < 1.

LaTeX

$$$$1 < \operatorname{inv}(a) \iff (0 < a \land a < 1)$$$$

Lean4

@[bound]
theorem inv_lt_one_of_one_lt₀ (ha : 1 < a) : a⁻¹ < 1 :=
  (inv_lt_one₀ <| zero_lt_one.trans ha).2 ha

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

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

Разделы

Аффилиация

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