supDegree_mem_range

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.supDegree_mem_range

← MathLib Explorer

English

The value p.supDegree D lies in the image of D.

Русский

Значение p.supDegree D принадлежит изображению D.

LaTeX

$$$p.supDegree D \in \operatorname{range} D$$$

Lean4

theorem supDegree_mem_range (hp : p ≠ 0) : p.supDegree D ∈ Set.range D := by
  obtain ⟨a, -, he⟩ := exists_supDegree_mem_support D hp; exact ⟨a, he.symm⟩

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

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

Разделы

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

Аффилиация

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