English
For any Finset s of α, an element o ∈ Option α lies in insertNone s if and only if every a ∈ o is already in s. In particular, none ∈ insertNone s for every s, and some a ∈ insertNone s exactly when a ∈ s.
Русский
Для любого множества Finset s из α элемент o ∈ Option α принадлежит insertNone s тогда и только тогда, когда каждый элемент a ∈ o уже принадлежит s. В частности, none ∈ insertNone s для любого s, а some a ∈ insertNone s тогда и только когда a ∈ s.
LaTeX
$$$o \\in \\text{insertNone}(s) \\;\\iff\\; \\forall a \\in o,\\ a \\in s$, где $o ∈ \\text{Option}(\\alpha)$. В частности, $\\text{none} \\in \\text{insertNone}(s)$ и $\\text{some}(a) \\in \\text{insertNone}(s) \\iff a \\in s$.$$
Lean4
@[simp]
theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s
| none => iff_of_true (Multiset.mem_cons_self _ _) fun a h => by cases h
| some a => Multiset.mem_cons.trans <| by simp
