Float

Mathlib.Data.FP.Basic

URI: https://scilib.ai/kg/mathlib#FP.Float

Lean4

@[nolint docBlame]
inductive Float
  | inf : Bool → Float
  | nan : Float
  | finite : Bool → ∀ e m, ValidFinite e m → Float

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

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

Разделы

Аффилиация

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