Icc_self

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.Icc_self

English

The closed interval Icc(a,a) consists of the singleton {a}.

Русский

Замкнутый интервал Icc(a,a) состоит из единичного множества {a}.

LaTeX

$$$ Icc\ a\ a = \{ a \} $$$

Lean4

@[simp]
theorem Icc_self (a : α) : Icc a a = { a } := by rw [Icc, Finset.Icc_self, Finset.singleton_val]

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

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

Разделы

Аффилиация

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