image_Iic

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#OrderEmbedding.image_Iic

English

If e is an order-embedding and the range of e is lower, then the image e''Iic a equals Iic (e a).

Русский

Если e — вложение порядка и образ e является нижним, тогда образ e''Iic a равен Iic (e a).

LaTeX

$$$e''Iic(a) = Iic(e(a))$$$

Lean4

theorem image_Iic (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) : e '' Iic a = Iic (e a) :=
  e.dual.image_Ici he a

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

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

Разделы

Аффилиация

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