one_lt_rOut_div_rIn

Mathlib.Analysis.Calculus.BumpFunction.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem one_lt_rOut_div_rIn {c : E} (f : ContDiffBump c) : 1 < f.rOut / f.rIn :=
  by
  rw [one_lt_div f.rIn_pos]
  exact f.rIn_lt_rOut

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

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

Разделы

Аффилиация

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