some_mem_insertNone — Mathlib

English

For any finite set s of α and any element a ∈ α, the statement some a is in insertNone s if and only if a ∈ s.

Русский

Для любого конечного множества s из α и элемента a ∈ α утверждение some a принадлежит insertNone s тогда и только тогда, когда a ∈ s.

LaTeX

$$$\\text{some}(a) \\in \\text{insertNone}(s) \\iff a \\in s$.$$

Lean4

theorem some_mem_insertNone {s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s := by simp

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