uIcc_injective_right

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.uIcc_injective_right

← MathLib Explorer

English

For a fixed a, the map b ↦ [[b, a]] is injective.

Русский

Для фиксированного a отображение b ↦ [[b, a]] инъективно.

LaTeX

$$$\text{Injective}\; (\lambda b, [[b, a]])$$$

Lean4

theorem uIcc_injective_right (a : α) : Injective fun b => [[b, a]] := fun b c h =>
  by
  rw [Finset.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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