subset_powerset_iff

Mathlib.Data.Set.Lattice

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

English

s is a subset of t's power set if and only if the union over s is contained in t.

Русский

s ⊆ 𝒫(t) тогда и только тогда, когда ⋃s ⊆ t.

LaTeX

$$$ s \subseteq \mathcal{P} t \iff \bigcup s \subseteq t $$$

Lean4

theorem subset_powerset_iff {s : Set (Set α)} {t : Set α} : s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t :=
  sUnion_subset_iff.symm

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

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

Разделы

Аффилиация

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