one_le_dite

Mathlib.Algebra.Notation.Lemmas

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

English

If ha and hb bound 1 from below for all h, then dite p a b is at least 1.

Русский

Если ha и hb ограничивают 1 снизу, то dite p a b не меньше 1.

LaTeX

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

Lean4

@[to_additive dite_nonneg]
theorem one_le_dite [LE α] (ha : ∀ h, 1 ≤ a h) (hb : ∀ h, 1 ≤ b h) : 1 ≤ dite p a b := by split; exacts [ha ‹_›, hb ‹_›]

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

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

Разделы

Аффилиация

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