monovary_const_left

Mathlib.Order.Monotone.Monovary

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

English

Monovary (const ι a) g holds for any a and g, since (const ι a) i = a and hence g i < g j implies a ≤ a.

Русский

Monovary (const ι a) g выполняется для любых a и g, так как (const ι a) i = a, и следовательно g i < g j → a ≤ a.

LaTeX

$$$Monovary (const\ ι\ a)\ g$$$

Lean4

theorem monovary_const_left (g : ι → β) (a : α) : Monovary (const ι a) g := fun _ _ _ => le_rfl

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

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

Разделы

Аффилиация

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