coe_succ_of_mem

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#coe_succ_of_mem

← MathLib Explorer

English

If succ ↑a ∈ s, then (succ a).1 = succ ↑a.

Русский

Если succ(↑a) ∈ s, то (succ a).1 = succ ↑a.

LaTeX

$$$$ \operatorname{succ}(a).1 = \operatorname{succ}(a.1) $$$$

Lean4

@[simp, norm_cast]
theorem coe_succ_of_mem [SuccOrder α] {a : s} (h : succ ↑a ∈ s) : (succ a).1 = succ ↑a := by
  classical
  change Subtype.val (dite ..) = _
  split_ifs <;> trivial

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

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

Разделы

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

Аффилиация

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