recENNReal_neg_coe_ennreal

Mathlib.Data.EReal.Operations

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

Lean4

axiom recENNReal_neg_coe_ennreal {motive : EReal → Sort*} (coe : ∀ x : ℝ≥0∞, motive x)
    (neg_coe : ∀ x : ℝ≥0∞, 0 < x → motive (-x)) {x : ℝ≥0∞} (hx : 0 < x) : recENNReal coe neg_coe (-x) = neg_coe x hx

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

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

Разделы

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

Аффилиация

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