agree_children — Mathlib

English

If x and y are agrees and i ≍ j, then their children at i and j agree.

Русский

Если x и y согласованы и i ≍ j, тогда их дети в точках i и j согласованы.

LaTeX

$$$\text{agree\_children}\ x\ y\ (h_0)\ (h_1) : \; \text{Agree} (\text{children}'\ x\ i) (\text{children}'\ y\ j) $$$

Lean4

theorem agree_children {n : ℕ} (x : CofixA F (succ n)) (y : CofixA F (succ n + 1)) {i j} (h₀ : i ≍ j) (h₁ : Agree x y) :
    Agree (children' x i) (children' y j) :=
  by
  obtain - | ⟨_, _, hagree⟩ := h₁; cases h₀
  apply hagree

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