uIcc_injective_right

Mathlib.Order.Interval.Set.UnorderedInterval

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

← MathLib Explorer

English

The map b ↦ uIcc(b, a) is injective for fixed a.

Русский

Отображение b ↦ uIcc(b,a) инъективно относительно b при фиксированном a.

LaTeX

$$$ \\text{Injective}(\\lambda b. uIcc(b,a)) $$$

Lean4

theorem uIcc_injective_right (a : α) : Injective fun b => uIcc b a := fun b c h =>
  by
  rw [Set.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