forall₂_refl

Mathlib.Data.List.Forall2

URI: https://scilib.ai/kg/mathlib#List.forall₂_refl

English

If Rₐ is reflexive, then for any list l the relation Forall₂ Rₐ l l holds.

Русский

Если Rₐ рефлексивна, то для любого списка l выполняется Forall₂ Rₐ l l.

LaTeX

$$$$ [IsRefl\\;\\alpha\\;R_a]\\;\\Rightarrow\\; \\forall l:\\text{List }\\alpha, \\ \\mathrm{Forall₂}\\ R_a\\ l\\ l. $$$$

Lean4

theorem forall₂_refl [IsRefl α Rₐ] (l : List α) : Forall₂ Rₐ l l :=
  forall₂_same.2 fun _ _ => refl _

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

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

Разделы

Аффилиация

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