У меня проблема с оператором if в сумме.
Я проверил решение в другом вопросе на если утверждения в isabelle, но это не помогло.
Вот пример:
theorem dummy:
fixes a :: "('a::comm_ring_1 poly)"
and B :: "(('a::comm_ring_1 poly)^'n∷finite^'n∷finite)"
shows "1=1"
proof-
{ fix i j
have "(∑k∈UNIV. if i = k then (B $ i $ j) else 0) = B $ i $ j" sorry
}
Как мне доказать лемму, где есть «извините»?
Теорема, которую вы ищете, setsum_delta:
finite ?S ⟹
(∑k∈?S. if k = ?a then ?b k else 0) =
(if ?a ∈ ?S then ?b ?a else 0)
Если вы напишете k = i вместо i = k в своей сумме, она даже может быть решена автоматически:
have "(∑k∈UNIV. if k = i then (B $ i $ j) else 0) = B $ i $ j"
by (simp add: setsum_delta)
Для этого очень полезна команда find_theorems. Если вы напечатаете
find_theorems "∑_∈_. if _ then _ else _"
Вы получаете setsum_delta как одно из совпадений - вот как я его нашел.
