eq_univ

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.eq_univ

English

If α is a subsingleton, any nonempty subset equals univ.

Русский

Если α — подмножество с одним элементом, любое непустое подмножество равно univ.

LaTeX

$$$[\text{Subsingleton } \alpha] \; s.Nonempty \rightarrow s = \mathrm{univ}$$$

Lean4

theorem eq_univ [Subsingleton α] : s.Nonempty → s = univ :=
  by
  rintro ⟨x, hx⟩
  exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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

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

Разделы

Аффилиация

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