instEmptyCollection

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.instEmptyCollection

English

There is an empty collection of sets, defined pointwise by ∅.

Русский

Существуют пустые коллекции множеств, задаваемые точечно как ∅.

LaTeX

$$$\\exists E: \\text{Index} \\to Set\\alpha \\text{ with } E(i) = \\varnothing\\text{ for all } i$$$

Lean4

instance : EmptyCollection (Set α) :=
  ⟨fun _ ↦ False⟩

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

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

Разделы

Аффилиация

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