some_mem

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.some_mem

English

For a nonempty set s, some_mem ensures the witness lies in s.

Русский

Для непустого множества s нечто подобное: существующий элемент принадлежит s.

LaTeX

$$∀ {h : s.Nonempty}, h.some ∈ s$$

Lean4

protected theorem some_mem (h : s.Nonempty) : h.some ∈ s :=
  Classical.choose_spec h

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

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

Разделы

Аффилиация

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