isRight_finSumNatEquiv_symm_apply

English

The right-ness indicator of the preimage under finSumNatEquiv symm is decided by n ≤ i.

Русский

Индикатор правой части предобраза под symm равен решению n ≤ i.

LaTeX

$$$ ((finSumNatEquiv n).symm i).isRight = \\mathrm{decide}(n \\le i) $$$

Lean4

@[simp]
theorem isRight_finSumNatEquiv_symm_apply (i : ℕ) : ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i) :=
  by
  simp_rw [← not_lt, decide_not, ← isLeft_finSumNatEquiv_symm_apply]
  cases (finSumNatEquiv n).symm i <;> rfl

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