isPartition_single_iff — Mathlib

English

For a single-box prepartition, IsPartition holds iff the singleton box equals I.

Русский

Для одиночного бокса в предразбиении IsPartition истинно тогда и только тогда, когда сингелтонный бокс равен I.

LaTeX

$$$ \text{isPartition_single_iff} (h : J \le I) : IsPartition (single I J h) \iff J = I. $$$

Lean4

@[simp]
theorem isPartition_single_iff (h : J ≤ I) : IsPartition (single I J h) ↔ J = I := by simp [isPartition_iff_iUnion_eq]

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