choose_fst_mem

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.choose_fst_mem

English

If hs is a nontrivial set, then hs.choose.fst ∈ s.

Русский

Если s не тривиально, то первый выбор свидетель принадлежит s.

LaTeX

$$$ hs.choose.fst ∈ s $$$

Lean4

protected theorem choose_fst_mem (hs : s.Nontrivial) : hs.choose.fst ∈ s :=
  hs.choose_spec.left

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

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

Разделы

Аффилиация

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