instNontrivialShrink

Mathlib.Logic.Small.Defs

URI: https://scilib.ai/kg/mathlib#instNontrivialShrink

English

If α is Small and Nontrivial, Shrink(α) is Nontrivial.

Русский

Если α мала и не тривиальна, Shrink(α) не тривиальна.

LaTeX

$$$(Small(\alpha) \land Nontrivial(\alpha)) \Rightarrow Nontrivial(Shrink(\alpha)).$$$

Lean4

instance {α : Type u} [Small.{v} α] [Nontrivial α] : Nontrivial (Shrink.{v} α) :=
  (equivShrink α).symm.nontrivial

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

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

Разделы

Аффилиация

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