erase_cons — Mathlib

English

If a ∉ s, then erasing b from the set formed by adjoining a to s equals adjoining a to erase s b.

Русский

Если a не принадлежит s, то удаление b из множества, полученного добавлением a к s, даёт множество, равное добавлению a к удалению b из s.

LaTeX

$$$$ \text{erase}(\text{cons } a\ s\ ha)\ b = \text{cons } a\ (\text{erase } s\ b)\ (\text{ha}\ \text{erase_subset } _ _ h). $$$$

Lean4

theorem erase_cons {s : Finset α} {a : α} (h : a ∉ s) : (s.cons a h).erase a = s := by grind

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