mem_eraseNone

Mathlib.Data.Finset.Option

URI: https://scilib.ai/kg/mathlib#Finset.mem_eraseNone

English

For a finite s of Option α and x ∈ α, x ∈ eraseNone(s) iff Some x ∈ s.

Русский

Для конечного s из Option α и x ∈ α, x ∈ eraseNone(s) тогда и только тогда, когда Some x ∈ s.

LaTeX

$$$x \\in \\text{eraseNone}(s) \\iff \\text{Some}(x) \\in s$$$

Lean4

@[simp]
theorem mem_eraseNone {s : Finset (Option α)} {x : α} : x ∈ eraseNone s ↔ some x ∈ s := by simp [eraseNone]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru