castLE_lt_castLE_iff

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.castLE_lt_castLE_iff

English

If n ≤ m, then i.castLE h < j.castLE h iff i < j for i, j ∈ Fin n.

Русский

Если n ≤ m, то i.castLE h < j.castLE h эквивално i < j для i, j ∈ Fin(n).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru