nonempty_Ici

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.nonempty_Ici

English

Ici a is nonempty for any a.

Русский

Ici a непусто для любого a.

LaTeX

$$$ (Ici(a)).Nonempty $$$

Lean4

@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem nonempty_Ici : (Ici a).Nonempty :=
  ⟨a, mem_Ici.2 le_rfl⟩

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

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

Разделы

Аффилиация

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