eq_univ_of_forall

Mathlib.Data.Set.Basic

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

English

(∀ x, x ∈ s) → s = univ

Русский

Если для всех x выполняется x ∈ s, то s = univ.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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