finAddFlip_apply_mk_right — Mathlib

English

If k ≥ m and k < m+n, then finAddFlip (⟨k, h₂⟩ : Fin (m+n)) = ⟨k - m, proof⟩, i.e. the first component is k - m.

Русский

Если k ≥ m и k < m+n, то finAddFlip (⟨k, h₂⟩ : Fin (m+n)) = ⟨k - m, доказательство⟩, то есть первая компонента равна k - m.

LaTeX

$$$ \\text{If } h_1: m \\le k \\text{ and } h_2: k < m+n, \\ \\mathrm{finAddFlip}(\\langle k,h_2\\rangle) = \\langle k-m, \\cdots \\rangle $$$

Lean4

@[simp]
theorem finAddFlip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
    finAddFlip (⟨k, h₂⟩ : Fin (m + n)) = ⟨k - m, by cutsat⟩ :=
  by
  convert @finAddFlip_apply_natAdd n ⟨k - m, by cutsat⟩ m
  simp [Nat.add_sub_cancel' h₁]

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