one_le_inv_iff₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

1 ≤ a⁻¹ iff 0 < a ∧ a ≤ 1.

Русский

1 ≤ a⁻¹ эквивалентно 0 < a ∧ a ≤ 1.

LaTeX

$$$$1 \le a^{-1} \iff (0 < a \land a \le 1).$$$$

Lean4

theorem one_le_inv_iff₀ : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1
    where
  mp h := ⟨inv_pos.1 (zero_lt_one.trans_le h), inv_inv a ▸ (inv_le_one₀ <| zero_lt_one.trans_le h).2 h⟩
  mpr h := (one_le_inv₀ h.1).2 h.2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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