eq_univ_of_forall

Mathlib.Data.Fintype.Defs

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

English

If every element of α lies in s, then s equals univ.

Русский

Если для каждого элемента α выполняется x ∈ s, то s = univ.

LaTeX

$$$$ (\forall x, x \in s) \Rightarrow s = \mathrm{univ} $$$$

Lean4

theorem eq_univ_of_forall : (∀ x, x ∈ s) → s = univ :=
  eq_univ_iff_forall.2

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

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

Разделы

Аффилиация

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