rel_head — Mathlib

English

If R is IsRefl and l is Pairwise R, then for any a ∈ l, R(head(l), a).

Русский

Если R рефлексивно и l является Pairwise R, то для любого a ∈ l, выполняется R(голова(l), a).

LaTeX

$$$[IsRefl\\;\\alpha\\;R] \\Rightarrow (h_1 : l.\\,Pairwise\\;R) \\Rightarrow (ha : a \\in l) \\Rightarrow R(\\text{head}(l), a).$$$

Lean4

theorem rel_head [IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) : R (l.head <| ne_nil_of_mem ha) a :=
  h₁.rel_head_of_rel_head_head ha (refl_of ..)

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