English
For any Finset s of α and any predicate p on Option α, the statement that p holds for every element of insertNone s is equivalent to p holding for none and p holding for every some a with a ∈ s.
Русский
Для любого множества Finset s из α и любого предиката p на Option α равносильно тому, что p выполняется для каждого элемента insertNone s, если и только если p выполняется для none и p выполняется для каждого some a, если a ∈ s.
LaTeX
$$$(\\forall o \\in \\text{insertNone}(s), p(o)) \\iff p(\\text{none}) \\land (\\forall a \\in s,\; p(\\text{some}(a))).$$$
Lean4
theorem forall_mem_insertNone {s : Finset α} {p : Option α → Prop} :
(∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p a := by simp [Option.forall]
