Extending a function from the complement of a singleton

In this file, we define Function.subtypeNeLift which allows to extend a (dependent) function defined on the complement of a singleton.

def Function.subtypeNeLift {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} (i₀ : ι) (f : (j : { i : ι // i ≠ i₀ }) → M ↑j) (x : M i₀) (i : ι) : M i

Given i₀ : ι and x : M i₀, this is the (dependent) map (i : ι) → M i whose value at i₀ is x and which extends a given map on the complement of {i₀}.

Equations

• Function.subtypeNeLift i₀ f x i = if h : i = i₀ then ⋯.mpr x else f ⟨i, h⟩

@[simp]

theorem Function.subtypeNeLift_self {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} (i₀ : ι) (f : (j : { i : ι // i ≠ i₀ }) → M ↑j) (x : M i₀) : subtypeNeLift i₀ f x i₀ = x

theorem Function.subtypeNeLift_of_neq {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} (i₀ : ι) (f : (j : { i : ι // i ≠ i₀ }) → M ↑j) (x : M i₀) (i : ι) (h : i ≠ i₀) : subtypeNeLift i₀ f x i = f ⟨i, h⟩

@[simp]

theorem Function.subtypeNeLift_restriction {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} (φ : (i : ι) → M i) (i₀ : ι) : subtypeNeLift i₀ (fun (i : { i : ι // i ≠ i₀ }) => φ ↑i) (φ i₀) = φ