eval_indicator_apply_eq_one — Mathlib

English

For any a, evaluating the indicator at a yields 1.

Русский

При любом отображении a на значение индикатор при подстановке дает 1.

LaTeX

$$eval a (indicator a) = 1$$

Lean4

theorem eval_indicator_apply_eq_one (a : σ → K) : eval a (indicator a) = 1 :=
  by
  nontriviality
  have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self, zero_pow this.ne', sub_zero,
    Finset.prod_const_one]

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