preimage

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsUpperSet.preimage

English

If s is upper and f is monotone, then the preimage f^{-1}(s) is upper.

Русский

Если s — верхнее множество и f монотонна, то прообраз f^{-1}(s) является верхним.

LaTeX

$$$IsUpperSet s \\to Monotone f \\to IsUpperSet (f^{-1}(s))$$$

Lean4

theorem preimage (hs : IsUpperSet s) {f : β → α} (hf : Monotone f) : IsUpperSet (f ⁻¹' s : Set β) := fun _ _ h =>
  hs <| hf h

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

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

Разделы

Аффилиация

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