invAux_notMem_invSet

Mathlib.SetTheory.Nimber.Field

URI: https://scilib.ai/kg/mathlib#Nimber.invAux_notMem_invSet

English

For all a, invAux(a) is not a member of invSet(a).

Русский

Для всех a, invAux(a) не принадлежит invSet(a).

LaTeX

$$$ invAux(a) \notin invSet(a) $$$

Lean4

theorem invAux_notMem_invSet (a : Nimber) : invAux a ∉ invSet a :=
  by
  rw [invAux]
  exact csInf_mem (invSet_nonempty a)

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

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

Разделы

Аффилиация

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