nontrivial_univ

Mathlib.Data.Set.Subsingleton

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

English

If α is nontrivial, then the universal set univ is nontrivial.

Русский

Если α не тривиален, то единичный универсум является не тривиальным.

LaTeX

$$[Nontrivial α] ⇒ (univ : Set α).Nontrivial$$

Lean4

theorem nontrivial_univ [Nontrivial α] : (univ : Set α).Nontrivial :=
  let ⟨x, y, hxy⟩ := exists_pair_ne α
  ⟨x, mem_univ _, y, mem_univ _, hxy⟩

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

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

Разделы

Аффилиация

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