empty_subset

Mathlib.Data.Set.Basic

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

English

The empty set is a subset of every set.

Русский

Пустое множество является подмножеством любого множества.

LaTeX

$$$$ \emptyset \subseteq s. $$$$

Lean4

@[simp]
theorem empty_subset (s : Set α) : ∅ ⊆ s :=
  nofun

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

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

Разделы

Аффилиация

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