decidableMem — Mathlib

English

Membership in μ is decidable; i.e. there is a decision procedure for x ∈ μ equivalent to x ∈ μ.cells.

Русский

Принадлежность к μ разрешима; то есть существует решение для x ∈ μ, эквивалентное x ∈ μ.cells.

LaTeX

$$$\forall \mu:\; DecidablePred\; (x\in \mu) \;\text{ is defined by }\; DecidablePred\; (x\in \mu.cells).$$$

Lean4

instance decidableMem (μ : YoungDiagram) : DecidablePred (· ∈ μ) :=
  inferInstanceAs (DecidablePred (· ∈ μ.cells))

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