refl

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Subset.refl

English

For every set a, a ⊆ a.

Русский

Для каждого множества a выполняется a ⊆ a.

LaTeX

$$$\\forall a\\subseteq\\alpha, \\ a\\subseteq a$$$

Lean4

@[refl]
theorem refl (a : Set α) : a ⊆ a := fun _ => id

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

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

Разделы

Аффилиация

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