mem_invSet_of_lt_invAux

Mathlib.SetTheory.Nimber.Field

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

← MathLib Explorer

English

If b < invAux(a), then b ∈ invSet(a).

Русский

Если b < invAux(a), то b ∈ invSet(a).

LaTeX

$$$ b < invAux(a) \Rightarrow b \in invSet(a) $$$

Lean4

theorem mem_invSet_of_lt_invAux (h : b < invAux a) : b ∈ invSet a :=
  by
  rw [invAux] at h
  have := notMem_of_lt_csInf h ⟨_, bot_mem_lowerBounds _⟩
  rwa [Set.notMem_compl_iff] at this

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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