optionEquivRight_X_some — Mathlib

English

Under the right equivalence, the variable X applied to a Some x corresponds to the variable X in the target polynomial ring.

Русский

При отображении справа переменная X applied to Some x соответствует переменной X в целевом кольце полиномов.

LaTeX

$$$\\operatorname{optionEquivRight} \\; R\\; S_1\\; (X(\\operatorname{Option.some} x)) = X x$$$

Lean4

theorem optionEquivRight_X_some (x : S₁) : optionEquivRight R S₁ (X (some x)) = X x := by
  simp [optionEquivRight_apply, aeval_X]

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