subset_of_mem_powerset

Mathlib.Data.Set.Basic

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

English

Let α be a type and s, x be sets. If x ∈ 𝒫(s), then x ⊆ s.

Русский

Пусть α — множество, a и s — подмножества; если x ∈ 𝒫(s), то x ⊆ s.

LaTeX

$$$ x \\in \\mathcal{P}(s) \\Rightarrow x \\subseteq s $$$

Lean4

theorem subset_of_mem_powerset {x s : Set α} (h : x ∈ 𝒫 s) : x ⊆ s :=
  @h

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

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

Разделы

Аффилиация

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