subset_pair_iff_eq

Mathlib.Data.Set.Insert

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

← MathLib Explorer

English

The powerset of a singleton {x} consists exactly of ∅ and {x}.

Русский

Лексическое множество подмножеств множества {x} состоит ровно из ∅ и {x}.

LaTeX

$$$\\mathcal{P}({x}) = \\{\\emptyset, {x}\\}$$$

Lean4

theorem subset_pair_iff_eq (hs : s.Nonempty) : s ⊆ { a, b } ↔ s = { a } ∨ s = { b } ∨ s = { a, b } := by
  rw [Set.subset_pair_iff_eq, or_iff_right]; exact hs.ne_empty

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

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

Разделы

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

Аффилиация

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