mem_replace

Mathlib.Data.List.AList

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

English

An element a' is in replace a b s iff it was in s originally.

Русский

Элемент a' принадлежит replace a b s тогда и только тогда, когда он принадлежал s.

LaTeX

$$a' \in replace(a,b,s) \iff a' \in s$$

Lean4

@[simp]
theorem mem_replace {a a' : α} {b : β a} {s : AList β} : a' ∈ replace a b s ↔ a' ∈ s := by
  rw [mem_keys, keys_replace, ← mem_keys]

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

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

Разделы

Аффилиация

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