lift'_principal

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.lift'_principal

English

If h is monotone, then (𝓟 s).lift' h = 𝓟 (h s).

Русский

Если h монотонно, то (𝓟 s).lift' h = 𝓟 (h s).

LaTeX

$$$ (hh : Monotone h) : (\\mathcal{P} s).lift' h = \\mathcal{P}(h s) $$$

Lean4

theorem lift'_principal {s : Set α} (hh : Monotone h) : (𝓟 s).lift' h = 𝓟 (h s) :=
  lift_principal <| monotone_principal.comp hh

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

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

Разделы

Аффилиация

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