unitBall

Mathlib.Analysis.Normed.Field.UnitBall

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

Lean4

/-- Unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`. -/
def unitBall (𝕜 : Type*) [NonUnitalSeminormedRing 𝕜] : Subsemigroup 𝕜
    where
  carrier := ball (0 : 𝕜) 1
  mul_mem' hx
    hy := by
    rw [mem_ball_zero_iff] at *
    exact (norm_mul_le _ _).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) hx hy.le)

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

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

Разделы

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

Аффилиация

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