English
For a predicate P and a single point a ∈ Subtype P with value m ∈ M, the extension of the singleton equals the singleton at a with the same value: (single a m).extendDomain = single a.val m.
Русский
Для подмножества P и элемента a ∈ Subtype P, имеющего значение m ∈ M, расширение области определения единичной функции равно единичной функции в исходной точке: (single a m).extendDomain = single a.val m.
LaTeX
$$$(\\mathrm{single} a m).\\extendDomain = \\mathrm{single} a.\\mathrm{val} m$$$
Lean4
@[simp]
theorem extendDomain_single (a : Subtype P) (m : M) : (single a m).extendDomain = single a.val m :=
by
ext a'
dsimp only [extendDomain_toFun]
obtain rfl | ha := eq_or_ne a' a.val
· simp_rw [single_eq_same, dif_pos a.prop]
· simp_rw [single_eq_of_ne ha, dite_eq_right_iff]
intro h
rw [single_eq_of_ne]
simp [Subtype.ext_iff, ha]
