nontrivial_of_univ_nontrivial

Mathlib.Data.Set.Subsingleton

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

English

If the universe (univ) is nontrivial, then α is nontrivial.

Русский

Если множество-тип единицей (univ) не тривиально, то сам тип α не тривиален.

LaTeX

$$(univ Nontrivial) ⇒ Nontrivial α$$

Lean4

theorem nontrivial_of_univ_nontrivial (h : (univ : Set α).Nontrivial) : Nontrivial α :=
  let ⟨x, _, y, _, hxy⟩ := h
  ⟨⟨x, y, hxy⟩⟩

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

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

Разделы

Аффилиация

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