vecCons

Mathlib.Order.Fin.Tuple

URI: https://scilib.ai/kg/mathlib#StrictAnti.vecCons

English

If f is strictly antitone and f(0) < a, then vecCons a f is strictly antitone.

Русский

Если f строго антитонична и f(0) < a, то vecCons a f строго антитонична.

LaTeX

$$$\text{StrictAnti}(\mathrm{vecCons}(a,f))\;\text{if}\; \text{StrictAnti}(f) \text{ and } f(0) < a$$$

Lean4

theorem vecCons (hf : StrictAnti f) (ha : f 0 < a) : StrictAnti (vecCons a f) :=
  strictAnti_vecCons.2 ⟨ha, hf⟩

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

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

Разделы

Аффилиация

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