extendWith_single_zero — Mathlib

English

The operation extendWith preserves a single value when the added value is zero.

Русский

Операция extendWith сохраняет единичный элемент, когда добавляемое значение равно нулю.

LaTeX

$$$(\\mathrm{single}(i,x)).\\mathrm{extendWith} 0 = \\mathrm{single}(\\mathrm{some}~i) x$$$

Lean4

@[simp]
theorem extendWith_single_zero [DecidableEq ι] [∀ i, Zero (α i)] (i : ι) (x : α (some i)) :
    (single i x).extendWith 0 = single (some i) x := by
  ext (_ | j)
  · rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _).symm]
  · rw [extendWith_some]
    obtain rfl | hij := Decidable.eq_or_ne j i
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

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