English
If a ∉ s, the map g ↦ Pi.cons s a b g is injective from functions on s to functions on insert a s.
Русский
Если a ∉ s, отображение g ↦ Pi.cons s a b g инъективно из функций на s в функции на insert a s.
LaTeX
$$$\\text{Cons injective}:\\; \\exists hs: a \\notin s \\Rightarrow \\text{Injective}(\\ lambda g: s \\to β \\| g\\mapsto Pi.cons s a b g).$$$
Lean4
theorem cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) : Function.Injective (Pi.cons s a b) :=
fun e₁ e₂ eq =>
@Multiset.Pi.cons_injective α _ δ a b s.1 hs _ _ <|
funext fun e =>
funext fun h =>
have :
Pi.cons s a b e₁ e (by simpa only [Multiset.mem_cons, mem_insert] using h) =
Pi.cons s a b e₂ e (by simpa only [Multiset.mem_cons, mem_insert] using h) :=
by rw [eq]
this
