le — Mathlib · SciLib

English

For any finpartition P of a, and any b that belongs to P.parts, we have b ≤ a. In words, every block of a finpartition lies below the top element a.

Русский

Для любого финразбиения P a и любого b, принадлежащего P.parts, выполняется b ≤ a. Иными словами, каждый блок разбиения не превышает верхнюю границу a.

LaTeX

$$$\forall P: \mathrm{Finpartition}(a),\forall b\in P.\text{parts},\ b \le a$$$

Lean4

protected theorem le {b : α} (hb : b ∈ P.parts) : b ≤ a :=
  (le_sup hb).trans P.sup_parts.le

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