instIsTransNatLeHAddOfNat

Mathlib.Data.Nat.Fib.Zeckendorf

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

English

If a,b,c ∈ ℕ with b+2 ≤ a and c+2 ≤ b, then c+4 ≤ a.

Русский

Пусть a,b,c ∈ ℕ такие, что b+2 ≤ a и c+2 ≤ b; тогда c+4 ≤ a.

LaTeX

$$$$ \forall a,b,c \in \mathbb{N},\ (b+2 \le a) \land (c+2 \le b) \Rightarrow (c+4 \le a). $$$$

Lean4

@[nolint defLemma docBlame]
local instance : IsTrans ℕ fun a b ↦ b + 2 ≤ a where trans _a _b _c hba hcb := hcb.trans <| le_self_add.trans hba

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

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

Разделы

Аффилиация

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