finSumNatEquiv_symm_apply_of_ge

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSumNatEquiv_symm_apply_of_ge

English

For i with i ≥ n, the inverse image under finSumNatEquiv n is inr (i - n).

Русский

Для i, если i ≥ n, обратное изображение под фин SumNat Equiv n равно inr (i - n).

LaTeX

$$$ {i : \\mathbb{N}} (hi : n \\le i) : (finSumNatEquiv n).symm i = \\mathrm{inr} (i - n) $$$

Lean4

@[simp]
theorem finSumNatEquiv_symm_apply_of_ge {i : ℕ} (hi : n ≤ i) : (finSumNatEquiv n).symm i = .inr (i - n) :=
  dif_neg (Nat.not_lt_of_ge hi)

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

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

Разделы

Аффилиация

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