mem_replace

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.mem_replace

English

As above, membership after replacement is unchanged: a' ∈ replace a b s ↔ a' ∈ s.

Русский

Как выше, членство после замены не меняется: a' ∈ replace a b s ↔ a' ∈ s.

LaTeX

$$$ a' \in replace\ a\ b\ s \iff a' \in s. $$$

Lean4

@[simp]
theorem mem_replace {a a' : α} {b : β a} {s : Finmap β} : a' ∈ replace a b s ↔ a' ∈ s :=
  induction_on s fun s => by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru