setLike

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.setLike

English

The image of Iic under the castLE map equals Iic of the image of a.

Русский

Образ множества Iic через отображение castLE равен Iic образу a.

LaTeX

$$$(Iic a).image (castLE h) = Iic (castLE h a)$$$

Lean4

instance setLike : SetLike (NonemptyInterval α) α
    where
  coe s := Icc s.fst s.snd
  coe_injective' := coeHom.injective

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

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

Разделы

Аффилиация

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