biUnion_top — Mathlib

English

The biUnion of the top prepartition, with the top prepartition assigned to each box, equals the original prepartition.

Русский

Объединение biUnion верхнего предразбиения, когда для каждого J отображение равно верхнему, возвращает исходное предразбиение.

LaTeX

$$(π.biUnion fun _ => ⊤) = π$$

Lean4

@[simp]
theorem biUnion_top : (π.biUnion fun _ => ⊤) = π := by
  ext
  simp

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