Theorems · Definition · combinatorics

Finset.Pi.cons

{α : Type u_1} →
  {δ : α → Sort v} →
    [inst : DecidableEq α] →
      (s : Finset α) → (a : α) → δ a → ((a : α) → a ∈ s → δ a) → (a' : α) → a' ∈ insert a s → δ a'

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.

Defined in

Mathlib.Data.Finset.Pi

Cited by

6 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq