default_eq_empty — Mathlib

English

In a lattice with bottom, the default Finpartition of ⊥ is equal to Finpartition.empty.

Русский

Для линейного частичного порядка с нижней границей значение по умолчанию для Finpartition ⊥ равно пустой Finpartition.

LaTeX

$$$\text{default} : \text{Finpartition}(\bot : \alpha) = \text{Finpartition.empty } \alpha$$$

Lean4

@[simp]
theorem default_eq_empty : (default : Finpartition (⊥ : α)) = Finpartition.empty α :=
  rfl

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