nontrivial

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.nontrivial

English

If e: α ≃ β and β is nontrivial, then α is nontrivial.

Русский

Если e: α ≃ β и β не тривиален, то α не тривиален.

LaTeX

$$$\forall e:\alpha \simeq \beta,\ Nontrivial(\beta) \Rightarrow Nontrivial(\alpha)$$$

Lean4

protected theorem nontrivial {α β} (e : α ≃ β) [Nontrivial β] : Nontrivial α :=
  e.surjective.nontrivial

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

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

Разделы

Аффилиация

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