English
There is a natural equivalence between the set of functions α→β that agree with a fixed function x0 on the p-subtype and the set of functions from the ¬p-subtype to β.
Русский
Существует естественное эквивалентное отображение между множеством функций α→β, которые совпадают с заданной функцией x0 на подтипе p, и множеством функций от подтипа ¬p к β.
LaTeX
$$$$\\{ x : α \\to β \\;\\big|\\; x \\circ \\mathrm{Subtype.val} = x_0 \\} \\ \\simeq\\ \\{ a : \\{ a \\;|\\; \\neg p a \\} \\to β \\}. $$$$
Lean4
/-- For a fixed function `x₀ : {a // p a} → β` defined on a subtype of `α`,
the subtype of functions `x : α → β` that agree with `x₀` on the subtype `{a // p a}`
is naturally equivalent to the type of functions `{a // ¬ p a} → β`. -/
@[simps]
def subtypePreimage : { x : α → β // x ∘ Subtype.val = x₀ } ≃ ({ a // ¬p a } → β)
where
toFun (x : { x : α → β // x ∘ Subtype.val = x₀ }) a := (x : α → β) a
invFun x := ⟨fun a => if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩, funext fun ⟨_, h⟩ => dif_pos h⟩
left_inv := fun ⟨x, hx⟩ =>
Subtype.val_injective <|
funext fun a => by
dsimp only
split_ifs
· rw [← hx]; rfl
· rfl
right_inv
x :=
funext fun ⟨a, h⟩ =>
show dite (p a) _ _ = _ by
dsimp only
rw [dif_neg h]
