termΙ

Mathlib.Order.Interval.Set.UnorderedInterval

URI: https://scilib.ai/kg/mathlib#Interval.termΙ

Lean4

/-- `Ι a b` denotes the open-closed interval with unordered bounds. Here, `Ι` is a capital iota,
distinguished from a capital `i`. -/
@[scoped term_parser 1000]
public meta def termΙ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Interval.termΙ 1024 (ParserDescr.symbol✝ "Ι")

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

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

Разделы

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

Аффилиация

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