erase_eq_iff_eq_insert

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.erase_eq_iff_eq_insert

English

If a ∈ s and ht : a ∉ t, then erase s a = t implies s = insert a t.

Русский

Если a ∈ s и a ∉ t, то erase s a = t эквивалентно s = insert a t.

LaTeX

$$hs : a ∈ s ∧ a ∉ t ⇒ (erase s a = t ↔ s = insert a t)$$

Lean4

theorem erase_eq_iff_eq_insert (hs : a ∈ s) (ht : a ∉ t) : erase s a = t ↔ s = insert a t := by aesop

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

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

Разделы

Аффилиация

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