one_lt_ite

Mathlib.Algebra.Notation.Lemmas

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

English

If ha: a h < 1 and hb: b h < 1 for all h, then ite p a b < 1.

Русский

Если для всех h выполнено a(h) < 1 и b(h) < 1, тогда ite p a b < 1.

LaTeX

$$[LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) → ite p a b < 1$$

Lean4

@[to_additive ite_pos]
theorem one_lt_ite [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b := by split <;> assumption

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

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

Разделы

Аффилиация

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