nonempty_boxes — Mathlib

English

If π is a partition of I, then the collection of its boxes is nonempty; there exists at least one J ∈ π with J ⊆ I.

Русский

Если π — разбиение I, то множество блоков разбиения непусто; существует по крайней мере один блок J ∈ π с J ⊆ I.

LaTeX

$$$\\text{If } \\pi \\text{ is a partition of } I, \\ \\pi.{boxes} \\neq \\emptyset.$$$

Lean4

theorem nonempty_boxes (h : π.IsPartition) : π.boxes.Nonempty :=
  let ⟨J, hJ, _⟩ := h _ I.upper_mem
  ⟨J, hJ⟩

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