vecCons

Mathlib.Order.Fin.Tuple

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

English

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

Русский

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

LaTeX

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

Lean4

theorem vecCons (hf : Antitone f) (ha : f 0 ≤ a) : Antitone (vecCons a f) :=
  antitone_vecCons.2 ⟨ha, hf⟩

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

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

Разделы

Аффилиация

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