cast_le_cast — Mathlib

English

Let n and m be natural numbers with n = m. For any a, b in Fin n, a.cast eq ≤ b.cast eq iff a ≤ b.

Русский

Пусть n, m — натуральные числа и n = m. Для любых a, b ∈ Fin n верно, что 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 \\le b.cast\\,eq \\iff a \\le b $$$$

Lean4

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

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