cast_lt_cast — Mathlib

English

Let n and m be natural numbers with n = m. For any a, b in Fin n, the order is preserved by casting along eq: a.cast eq < b.cast eq if and only if a < b.

Русский

Пусть n, m — натуральные числа и n = m. Для любых a, b ∈ Fin n верно, что преобразование cast по равенству eq сохраняет порядок: a.cast eq < b.cast eq тогда и только тогда, когда a < b.

LaTeX

$$$$ \\forall \\{n,m : \\mathbb{N}\\} (eq : n = m) \\{a,b : \\mathrm{Fin}\\,n\\}, a.cast\\,eq < b.cast\\,eq \\iff a < b $$$$

Lean4

@[simp]
theorem cast_lt_cast (eq : n = m) {a b : Fin n} : a.cast eq < b.cast eq ↔ a < b :=
  Iff.rfl

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