agree'_refl — Mathlib

English

For every n, any x ∈ M F satisfies Agree' n x x (reflexivity of the agreement relation).

Русский

Для любого n верно Agree' n x x (рефлексивность отношения согласованности).

LaTeX

$$$\\operatorname{agree'}\\_\\mathrm{refl} \\\\{n : \\mathbb{N}\\} (x : M F) : \\operatorname{Agree'} n x x$$$

Lean4

@[simp]
theorem agree'_refl {n : ℕ} (x : M F) : Agree' n x x :=
  by
  induction n generalizing x with
        | zero => ?_
        | succ _ n_ih => ?_ <;>
        induction x using PFunctor.M.casesOn' <;>
      constructor <;>
    try rfl
  intro; apply n_ih

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