instInvolutiveNeg

Mathlib.Data.EReal.Operations

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

Lean4

instance : InvolutiveNeg EReal where
  neg_neg
    a :=
    match a with
    | ⊥ => rfl
    | ⊤ => rfl
    | (a : ℝ) => congr_arg Real.toEReal (neg_neg a)

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

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

Разделы

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

Аффилиация

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