isGood_nil

Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.Products.isGood_nil

← MathLib Explorer

English

The nil product is good for the singleton {false}.

Русский

Nil-произведение является хорошим для единичного множества {false}.

LaTeX

$$$$\\mathrm{Products.isGood}\\; (\\{\\mathrm{false}\\}\\, )\\; \\mathrm{nil}$$$$

Lean4

theorem isGood_nil {I} [LinearOrder I] : Products.isGood ({fun _ ↦ false} : Set (I → Bool)) Products.nil :=
  by
  intro h
  simp [Products.eval, Products.nil] at h

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

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

Разделы

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

Аффилиация

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