LiftR_RelLast_iff

Mathlib.Control.Functor.Multivariate

URI: https://scilib.ai/kg/mathlib#MvFunctor.LiftR_RelLast_iff

Lean4

theorem LiftR_RelLast_iff (x y : F (α ::: β)) : LiftR' (RelLast' _ rr) x y ↔ LiftR (RelLast _ rr) x y :=
  by
  dsimp only [LiftR, LiftR']
  apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
  · ext i ⟨x, _⟩ : 2
    cases i <;> rfl
  · intros
    simp +unfoldPartialApp only [map_map, TypeVec.comp]
    apply iff_of_eq
    congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

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

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

Разделы

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

Аффилиация

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