zero_mem_invSet

Mathlib.SetTheory.Nimber.Field

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

English

0 belongs to the inverse set of every a; i.e., 0 ∈ invSet(a).

Русский

0 принадлежит множеству обратного элемента для любого a; то есть 0 ∈ invSet(a).

LaTeX

$$$0 \in invSet(a)$$$

Lean4

theorem zero_mem_invSet (a : Nimber) : 0 ∈ invSet a :=
  by
  rw [invSet]
  exact Set.mem_sInter.2 fun _ hs => hs.1

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

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

Разделы

Аффилиация

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