restrict_dite — Mathlib

English

The restriction with a conditional (dite) expression equals a straightforward function on the subtype, by case analysis on membership.

Русский

Ограничение с использованием условного выражения (dite) эквивалентно простой функции на подтипе, по разбору по членству.

LaTeX

$$$s.restrict (\lambda a : α, \lambda h, \beta) = (\lambda a : s, f a.2)$$$

Lean4

@[simp]
theorem restrict_dite {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 => f a a.2) :=
  funext fun a => dif_pos a.2

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