subset_univ

Mathlib.Data.Fintype.Defs

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

English

Any Finset s is a subset of univ.

Русский

Любой Finset s является подмножеством univ.

LaTeX

$$$$ s \subseteq \mathrm{univ} $$$$

Lean4

@[simp]
theorem subset_univ (s : Finset α) : s ⊆ univ := fun a _ => mem_univ a

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

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

Разделы

Аффилиация

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