symm

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.subsingleton.symm

English

If α is Subsingleton, then β is Subsingleton for e: α ≃ β.

Русский

Если α пододномен, то β тоже пододномен при эвалюции e: α ≃ β.

LaTeX

$$$e: \alpha \simeq \beta \Rightarrow [Subsingleton \alpha] \Rightarrow Subsingleton \beta$$$

Lean4

protected theorem symm (e : α ≃ β) [Subsingleton α] : Subsingleton β :=
  e.symm.injective.subsingleton

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

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

Разделы

Аффилиация

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