seminormFromConst_one_le

Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

URI: https://scilib.ai/kg/mathlib#seminormFromConst_one_le

← MathLib Explorer

English

The bound seminormFromConst' hf1 hc hpm 1 ≤ 1 holds (i.e., the value at 1 is not greater than 1).

Русский

Промежуточная граница: seminormFromConst' hf1 hc hpm 1 ≤ 1.

LaTeX

$$$\operatorname{seminormFromConst'} hf1 hc hpm 1 \le 1$$$

Lean4

/-- `seminormFromConst' hf1 hc hpm 1 ≤ 1`. -/
theorem seminormFromConst_one_le : seminormFromConst' hf1 hc hpm 1 ≤ 1 :=
  le_of_eq (seminormFromConst_one hf1 hc hpm)

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

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

Разделы

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

Аффилиация

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