coe_inj

Mathlib.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#Interval.coe_inj

English

For s,t in NonemptyInterval α, (s as Interval α) = t if and only if s = t.

Русский

Для s,t ∈ NonemptyInterval α верно: (s как Interval α) = t тогда и только тогда, когда s = t.

LaTeX

$$$ (s : \mathrm{Interval}(\alpha)) = t \;\iff\; s = t $$$

Lean4

@[norm_cast]
theorem coe_inj {s t : NonemptyInterval α} : (s : Interval α) = t ↔ s = t :=
  WithBot.coe_inj

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

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

Разделы

Аффилиация

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