coe_consEquiv_of_ne

Mathlib.Data.Multiset.Fintype

URI: https://scilib.ai/kg/mathlib#Multiset.coe_consEquiv_of_ne

← MathLib Explorer

English

If the head of x is not v, then consEquiv x = some ⟨x.1, x.2.cast(… )⟩.

Русский

Если голова x не равна v, то consEquiv x = some ⟨x.1, x.2.cast(… )⟩.

LaTeX

$$$\text{coe\_consEquiv\_of\_ne}(x) = \text{some } \langle x.1, x.2.cast(\text{...}) \rangle$$$

Lean4

theorem coe_consEquiv_of_ne {v : α} (x : v ::ₘ m) (hx : ↑x ≠ v) : consEquiv x = some ⟨x.1, x.2.cast (by simp [hx])⟩ :=
  by
  simp [consEquiv, hx]
  rfl

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

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

Разделы

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

Аффилиация

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