nonempty_congr

Mathlib.Logic.Equiv.Defs

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

English

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

Русский

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

LaTeX

$$$\forall e:\alpha \simeq \beta, Nonempty \alpha \iff Nonempty \beta$$$

Lean4

theorem nonempty_congr (e : α ≃ β) : Nonempty α ↔ Nonempty β :=
  Nonempty.congr e e.symm

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

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

Разделы

Аффилиация

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