insertNone_nonempty

Mathlib.Data.Finset.Option

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

← MathLib Explorer

English

The image insertNone(s) is nonempty, as it contains none.

Русский

Образ insertNone(s) непуст: он содержит none.

LaTeX

$$$\\text{insertNone}(s) \\;\\text{Nonempty}$$$

Lean4

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem insertNone_nonempty {s : Finset α} : insertNone s |>.Nonempty :=
  ⟨none, none_mem_insertNone⟩

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

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

Разделы

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

Аффилиация

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