instDecidableLE — Mathlib

English

The Colex order on Finset α is decidable once α carries a decidable order and equality; i.e., one can algorithmically determine which of two Colex elements is larger or if they are equal.

Русский

Порядок Коэкса на конечных множествах α разрешим: при наличии разрешимого порядка и равенства на α можно вычислить, какое из двух элементов Коэкса больше (или они равны).

LaTeX

$$$$ \\text{DecidableLE}(\\operatorname{Colex}(\\mathsf{Finset}(\\alpha))) $$$$

Lean4

instance instDecidableLE [DecidableLE α] : DecidableLE (Colex (Finset α)) := fun s t ↦
  decidable_of_iff' (∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b) Iff.rfl

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