one_lt_dite

Mathlib.Algebra.Notation.Lemmas

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

English

If ha: ∀ h, 1 < a h and hb: ∀ h, 1 < b h, then 1 < dite p a b.

Русский

Если ha: ∀ h, 1 < a h и hb: ∀ h, 1 < b h, то 1 < dite p a b.

LaTeX

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

Lean4

@[to_additive dite_pos]
theorem one_lt_dite [LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b := by split; exacts [ha ‹_›, hb ‹_›]

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

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

Разделы

Аффилиация

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