castLE_le_castLE_iff — Mathlib

English

If n ≤ m, then for i, j ∈ Fin n, i.castLE h ≤ j.castLE h iff i ≤ j. In other words, Fin.castLE with h embeds Fin n into Fin m as an order-embedding.

Русский

Пусть n ≤ m. Тогда для любых i, j ∈ Fin(n) выполняется i.castLE h ≤ j.castLE h, если и только i ≤ j. То есть Fin.castLE с сохранением порядка является вложением.

LaTeX

$$$\forall {m n : \mathbb{N}} {i j : \mathrm{Fin}(n)} (h : n \le m), i.castLE h \le j.castLE h \iff i \le j$$$

Lean4

@[simp]
theorem castLE_le_castLE_iff {i j : Fin n} (h : n ≤ m) : i.castLE h ≤ j.castLE h ↔ i ≤ j :=
  .rfl

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