eq_univ_iff_forall

Mathlib.Data.Fintype.Defs

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

English

A Finset s equals univ if and only if every element belongs to s.

Русский

Финитный набор s равен univ тогда, когда каждый элемент принадлежит s.

LaTeX

$$$$ s = \mathrm{univ} \iff \forall x, x \in s $$$$

Lean4

theorem eq_univ_iff_forall : s = univ ↔ ∀ x, x ∈ s := by simp [Finset.ext_iff]

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

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

Разделы

Аффилиация

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