coe_eraseNone

Mathlib.Data.Finset.Option

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

English

As sets, eraseNone s equals the preimage under the injection Some of s.

Русский

Как множества, eraseNone s равен предобразованию под внедрением Some от s.

LaTeX

$$$\\big(eraseNone(s)\\big) = \\text{Some}^{-1}(s)$$$

Lean4

@[simp]
theorem coe_eraseNone (s : Finset (Option α)) : (eraseNone s : Set α) = some ⁻¹' s :=
  Set.ext fun _ => mem_eraseNone

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

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

Разделы

Аффилиация

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