English
Let s be a subset of α. For any function f defined on s and any function g defined on the complement of s, form a function h on the whole space by h(a) = f(a) if a ∈ s and h(a) = g(a) if a ∉ s. Then the restriction of h to the complement sᶜ is exactly the function a ↦ g(a) with the evident proof a ∉ s.
Русский
Пусть s ⊆ α. Для функции f на s и функции g на дополнении к s образуется функция h на всей области: h(a) = f(a) при a ∈ s, и h(a) = g(a) при a ∉ s. Тогда ограничение h на дополнение sᶜ совпадает с функцией a ↦ g(a), где доказательство a ∉ s используется внутри.
LaTeX
$$$\\bigl(s^{\\complement}\\bigr)\\restrict \\bigl( a \\mapsto \\text{if } a \\in s \\text{ then } f\\,a\\,\\text{else } g\\,a \\bigr) \;=\\; \\lambda a:(s^{\\complement}: Set\\ α) \\;=>\\; g\\; a\, a.2$$
Lean4
@[simp]
theorem restrict_dite_compl {s : Set α} [∀ x, Decidable (x ∈ s)] (f : ∀ a ∈ s, β) (g : ∀ a ∉ s, β) :
(sᶜ.restrict fun a => if h : a ∈ s then f a h else g a h) = (fun a : (sᶜ : Set α) => g a a.2) :=
funext fun a => dif_neg a.2
