inv_pos_of_pos_ne_top

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.inv_pos_of_pos_ne_top

← MathLib Explorer

English

If 0 < a and a ≠ ⊤, then 0 < a^{-1}.

Русский

Если 0 < a и a ≠ ⊤, то 0 < a^{-1}.

LaTeX

$$$ 0 < a \text{ and } a \neq \top \Rightarrow 0 < a^{-1} $$$

Lean4

theorem inv_pos_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹ :=
  by
  lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_pos_of_pos h

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

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

Разделы

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

Аффилиация

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