monotone_powerset

Mathlib.Data.Set.Basic

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

English

The powerset operator is monotone as a function from Set α to Set(Set α).

Русский

Оператор подмножеств монотонен как отображение Set α → Set(Set α).

LaTeX

$$$ \\forall s,t \\, ( s \\subseteq t \\Rightarrow \\mathcal{P}(s) \\subseteq \\mathcal{P}(t) )$$$

Lean4

theorem monotone_powerset : Monotone (powerset : Set α → Set (Set α)) := fun _ _ => powerset_mono.2

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

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

Разделы

Аффилиация

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