antitone_vecCons

Mathlib.Order.Fin.Tuple

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

English

Antitone vecCons a f iff f(0) ≤ a and f is antitone.

Русский

Антиупорядоченность vecCons a f эквивалентна f(0) ≤ a и f антимонотонна.

LaTeX

$$$\text{Antitone}(\text{vecCons } a f) \iff f(0) \le a \land \text{Antitone} f.$$$

Lean4

@[simp]
theorem antitone_vecCons : Antitone (vecCons a f) ↔ f 0 ≤ a ∧ Antitone f :=
  monotone_vecCons (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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