le_one

Mathlib.Analysis.Calculus.BumpFunction.Basic

URI: https://scilib.ai/kg/mathlib#ContDiffBump.le_one

English

The ratio rOut/rIn is greater than 1: 1 < f.rOut/f.rIn.

Русский

Отношение rOut/rIn больше единицы: 1 < f.rOut/f.rIn.

LaTeX

$$$ 1 < \dfrac{f.rOut}{f.rIn}. $$$

Lean4

theorem le_one : f x ≤ 1 :=
  (ContDiffBumpBase.mem_Icc (someContDiffBumpBase E) _ _).2

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

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

Разделы

Аффилиация

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