nadd_le_iff — Mathlib

English

A closed form for the order relation b ♯ c ≤ a in terms of all smaller left and right parts.

Русский

Коэффициентная форма для отношения порядка b ♯ c ≤ a через все меньшие слева и справа части.

LaTeX

$$$b \# c \le a \iff (\forall b' < b,\ b' \# c < a) \land (\forall c' < c,\ b \# c' < a)$$$

Lean4

theorem nadd_le_iff : b ♯ c ≤ a ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a :=
  by
  rw [← not_lt, lt_nadd_iff]
  simp

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