nontrivial_congr

Mathlib.Logic.Equiv.Defs

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

English

For e: α ≃ β, Nontrivial α ↔ Nontrivial β.

Русский

Для e: α ≃ β, Nontrivial α эквивалентно Nontrivial β.

LaTeX

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

Lean4

theorem nontrivial_congr {α β} (e : α ≃ β) : Nontrivial α ↔ Nontrivial β :=
  ⟨fun _ ↦ e.symm.nontrivial, fun _ ↦ e.nontrivial⟩

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

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

Разделы

Аффилиация

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