isLeft_finSumNatEquiv_symm_apply — Mathlib

English

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

Русский

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

LaTeX

$$$ ((finSumNatEquiv n).symm i).isLeft = \\mathrm{decide}(i < n) $$$

Lean4

@[simp]
theorem isLeft_finSumNatEquiv_symm_apply (i : ℕ) : ((finSumNatEquiv n).symm i).isLeft = decide (i < n) :=
  by
  rcases i.lt_or_ge n with hi | hi
  · simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]
  · simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]

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