ne_singleton

Mathlib.Data.Set.Subsingleton

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

English

If s is nontrivial, then s ≠ {a} for any a.

Русский

Если множество s не тривиально, то оно не равно {a} для любого a.

LaTeX

$$∀ {a}, s.Nontrivial → s ≠ {a}$$

Lean4

theorem ne_singleton {x} (hs : s.Nontrivial) : s ≠ { x } := fun H =>
  by
  rw [H] at hs
  exact not_nontrivial_singleton hs

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

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

Разделы

Аффилиация

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