one_le_extend

Mathlib.Algebra.Order.Pi

URI: https://scilib.ai/kg/mathlib#Function.one_le_extend

← MathLib Explorer

English

If 1 ≤ g and 1 ≤ e, then 1 ≤ extend f g e.

Русский

Если 1 ≤ g и 1 ≤ e, то 1 ≤ extend f g e.

LaTeX

$$$\\forall f,g,e,\\ (1 \\le g) \\land (1 \\le e) \\Rightarrow 1 \\le \\mathrm{extend}(f,g,e).$$$

Lean4

@[to_additive extend_nonneg]
theorem one_le_extend (hg : 1 ≤ g) (he : 1 ≤ e) : 1 ≤ extend f g e := fun _b ↦ by
  classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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