Ici_injective

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_injective

English

The function from α to the lattice of upper sets sending a to Ici(a) is injective.

Русский

Функция из α в решетку верхних множеств, отправляющая a в Ici(a), инъективна.

LaTeX

$$$\text{Injective}(\mathrm{Ici})$$$

Lean4

nonrec theorem Ici_injective : Injective (Ici : α → UpperSet α) := fun _a _b hab ↦
  Ici_injective <| congr_arg ((↑) : _ → Set α) hab

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

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

Разделы

Аффилиация

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