English
Given a function f on s, extend it to s ∪ {a} by assigning a new value b to a, while keeping f on s unchanged.
Русский
Дано f на s, расширяем его до s ∪ {a}, присваивая значение b элементу a и сохраняем значения на s.
LaTeX
$$$ \\text{Pi.cons}(s,a,b,f) : (a' \\in insert a s) \\mapsto \\begin{cases} b & a'=a \\\\ f(a') & \\text{если } a' \\in s \end{cases}$. $$
Lean4
/-- Given a function `f` defined on a finset `s`, define a new function on the finset `s ∪ {a}`,
equal to `f` on `s` and sending `a` to a given value `b`. This function is denoted
`s.Pi.cons a b f`. If `a` already belongs to `s`, the new function takes the value `b` at `a`
anyway. -/
def cons (s : Finset α) (a : α) (b : δ a) (f : ∀ a, a ∈ s → δ a) (a' : α) (h : a' ∈ insert a s) : δ a' :=
Multiset.Pi.cons s.1 a b f _ (Multiset.mem_cons.2 <| mem_insert.symm.2 h)
