mem_top — Mathlib

English

The top prepartition of I contains only the whole box I; i.e., a box J belongs to the top prepartition if and only if J = I.

Русский

Верхнее предразбиение для I содержит только самую большую коробку I; то есть коробка J принадлежит верхнему предразбиению тогда и только тогда, когда J = I.

LaTeX

$$$J \in \mathrm{Top}(I) \iff J = I$$$

Lean4

@[simp]
theorem mem_top : J ∈ (⊤ : Prepartition I) ↔ J = I :=
  mem_singleton

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