Iic_injective

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#LowerSet.Iic_injective

English

The map a ↦ Iic a is injective: if Iic a = Iic b, then a = b.

Русский

Функция a ↦ Iic a инъективна: если Iic a = Iic b, то a = b.

LaTeX

$$Iic a = Iic b \Rightarrow a = b$$

Lean4

nonrec theorem Iic_injective : Injective (Iic : α → LowerSet α) := fun _a _b hab ↦
  Iic_injective <| congr_arg ((↑) : _ → Set α) hab

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

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

Разделы

Аффилиация

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