isPartition_single_iff — Mathlib

English

The singleton prepartition (the one containing only J) is a partition if and only if J = I.

Русский

Единичное разбиение (содержащее только J) является разбиением тогда и только тогда, когда J = I.

LaTeX

$$$ (single\,I\,J\,hJ\,x\,h).IsPartition \iff J = I $$$

Lean4

theorem isPartition_single_iff (hJ : J ≤ I) (h : x ∈ Box.Icc I) : (single I J hJ x h).IsPartition ↔ J = I :=
  Prepartition.isPartition_single_iff hJ

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