lex_le_iff_of_unique — Mathlib

English

If α has a Unique instance, then for a,b ∈ Lex(α →₀ N), a ≤ b iff ofLex a default ≤ ofLex b default.

Русский

Если у α имеется уникальный элемент, то для любых a,b ∈ Lex(α →₀ N) выполняется a ≤ b тогда и только тогда, когда ofLex a default ≤ ofLex b default.

LaTeX

$$$a \\le b \\iff \\operatorname{ofLex} a default \\le \\operatorname{ofLex} b default$$$

Lean4

theorem lex_le_iff_of_unique [Unique α] {a b : Lex (α →₀ N)} : a ≤ b ↔ ofLex a default ≤ ofLex b default :=
  by
  simp only [le_iff_eq_or_lt]
  apply or_congr _ lex_lt_iff_of_unique
  conv_lhs => rw [← toLex_ofLex a, ← toLex_ofLex b, toLex_inj]
  simp only [Finsupp.ext_iff, Unique.forall_iff]

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