erase_cons_of_ne — Mathlib

English

If a ∉ s and a ≠ b, then erasing b from the cons(a, s) equals cons(a, erase(s, b)). In set terms, erasing b from {a} ∪ s with a ∉ s and a ≠ b yields {a} ∪ (s \\ {b}).

Русский

Если a ∉ s и a ≠ b, то стирание b из {a} ∪ s равно {a} ∪ (s \ {b}).

LaTeX

$$$(a \\notin s) \\land (a \\neq b) \\Rightarrow \\operatorname{erase}(\\{a\\} \\cup s, b) = \\{a\\} \\cup \\operatorname{erase}(s,b)$$$

Lean4

theorem erase_cons_of_ne {a b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) :
    erase (cons a s ha) b = cons a (erase s b) fun h => ha <| erase_subset _ _ h := by grind

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