sdiff_singleton_wcovBy

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#Set.sdiff_singleton_wcovBy

← MathLib Explorer

English

For any set s and element a, s \ {a} is weakly covered by s.

Русский

Для любых множества s и элемента a, s \ {a} слабo покрывает s.

LaTeX

$$s \ { a } \mathrm{WCovBy} s$$

Lean4

@[simp]
theorem sdiff_singleton_wcovBy (s : Set α) (a : α) : s \ { a } ⩿ s :=
  by
  by_cases ha : a ∈ s
  · convert wcovBy_insert a _
    ext
    simp [ha]
  · simp [ha]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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