lowerBounds_image

Mathlib.Order.Bounds.OrderIso

URI: https://scilib.ai/kg/mathlib#OrderIso.lowerBounds_image

English

Let f : α ≃o β. Then the lower bounds of the image satisfy: lowerBounds(f''s) = f''(lowerBounds(s)).

Русский

Пусть f : α ≃o β. Тогда нижние границы образа удовлетворяют: lowerBounds(f''s) = f''(lowerBounds(s)).

LaTeX

$$$lowerBounds(f''s) = f''(lowerBounds(s)).$$$

Lean4

theorem lowerBounds_image {s : Set α} : lowerBounds (f '' s) = f '' lowerBounds s :=
  @upperBounds_image αᵒᵈ βᵒᵈ _ _ f.dual _

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

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

Разделы

Аффилиация

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