decidableEqOfDecidableLE — Mathlib

English

If there is a decidable ≤ on α, then equality on α is decidable.

Русский

Если на α задано разрешимое отношение ≤, то равенство на α разрешимо.

LaTeX

$$$[DecidableLE \alpha] \rightarrow DecidableEq \alpha$$$

Lean4

/-- Equality is decidable if `≤` is. -/
def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
  | a, b =>
    if hab : a ≤ b then if hba : b ≤ a then isTrue (le_antisymm hab hba) else isFalse fun heq => hba (heq ▸ le_refl _)
    else
      isFalse fun heq =>
        hab
          (heq ▸ le_refl _)
            -- See Note [decidable namespace]

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