finCongr_apply_mk — Mathlib

English

If h : m = n, k : Nat, hk : k < m, then finCongr h( Fin.mk(k, hk) ) = Fin.mk(k, h ▸ hk).

Русский

Если h : m = n, k : нат, hk : k < m, тогда finCongr h( Fin.mk(k, hk) ) = Fin.mk(k, h ▸ hk).

LaTeX

$$$$ \\operatorname{finCongr}(h)\\bigl(\\operatorname{Fin.mk}(k, hk)\\bigr) = \\operatorname{Fin.mk}(k, h \\; \\triangleright\\; hk). $$$$

Lean4

@[simp]
theorem _root_.finCongr_apply_mk (h : m = n) (k : ℕ) (hk : k < m) : finCongr h ⟨k, hk⟩ = ⟨k, h ▸ hk⟩ :=
  rfl

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