unitClosedBall

Mathlib.Analysis.Normed.Field.UnitBall

URI: https://scilib.ai/kg/mathlib#Subsemigroup.unitClosedBall

Lean4

/-- Closed unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`. -/
def unitClosedBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] : Subsemigroup 𝕜
    where
  carrier := closedBall 0 1
  mul_mem' hx
    hy := by
    rw [mem_closedBall_zero_iff] at *
    exact (norm_mul_le _ _).trans (mul_le_one₀ hx (norm_nonneg _) hy)

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

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

Разделы

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

Аффилиация

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