choose_fst_ne_choose_snd

Mathlib.Data.Set.Subsingleton

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

English

The first witness and the second witness are distinct: hs.choose.fst ≠ hs.choose.snd.

Русский

Первый и второй свидетели различны: hs.choose.fst ≠ hs.choose.snd.

LaTeX

$$$ hs.choose.fst \neq hs.choose.snd $$$

Lean4

protected theorem choose_fst_ne_choose_snd (hs : s.Nontrivial) : hs.choose.fst ≠ hs.choose.snd :=
  hs.choose_spec.right.choose_spec.right

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

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

Разделы

Аффилиация

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