cons_ne — Mathlib

English

If a ≠ a', then evaluating Pi.cons at a' gives f(a') with the appropriate restriction.

Русский

Если a ≠ a', то значение Pi.cons на a' равно f(a') с соответствующим ограничением.

LaTeX

$$$ Pi.cons(s,a,b,f)\\, a'\\;h = f(a') ((mem_insert.1 h).resolve_left( ha.symm )) \\text{ при } a \\neq a'. $$$

Lean4

theorem cons_ne {s : Finset α} {a a' : α} {b : δ a} {f : ∀ a, a ∈ s → δ a} {h : a' ∈ insert a s} (ha : a ≠ a') :
    Pi.cons s a b f a' h = f a' ((mem_insert.1 h).resolve_left ha.symm) :=
  Multiset.Pi.cons_ne _ (Ne.symm ha)

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