coe_covBy_iff — Mathlib

English

CovBy in Fin n is compatible with CovBy in ℕ via the natural coercion.

Русский

Связь покрытия в Fin n согласуется с той же связью в ℕ через естественное вложение.

LaTeX

$$$a \CovBy b \iff a.\\val \CovBy b.\\val \quad (a,b \\in \\mathrm{Fin}(n)).$$$

Lean4

@[simp, norm_cast]
theorem coe_covBy_iff {n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b ↔ a ⋖ b :=
  and_congr_right' ⟨fun h _c hc => h hc, fun h c ha hb => @h ⟨c, hb.trans b.prop⟩ ha hb⟩

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