is_refl — Mathlib

English

If Rₐ is reflexive, then every list l has SublistForall₂ Rₐ relating l.tail to l, i.e., the tail is related to the full list by Forall₂ with respect to Rₐ.

Русский

Если Rₐ рефлексивно, то каждый список l удовлетворяет SublistForall₂ Rₐ между хвостом l и самим списком, то есть хвост связан с полным списком отношением Forall₂ по Rₐ.

LaTeX

$$$$\\text{SublistForall₂.is\_refl: } [IsRefl\\; α\\ R_\\alpha] \\Rightarrow \\text{List.tail} \\;\\text{l} \; \\mathrm{SublistForall₂}\\; R_\\alpha \\; \\text{l}.$$$$

Lean4

instance is_refl [IsRefl α Rₐ] : IsRefl (List α) (SublistForall₂ Rₐ) :=
  ⟨fun l => sublistForall₂_iff.2 ⟨l, forall₂_refl l, Sublist.refl l⟩⟩

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