ofEq_apply — Mathlib

English

If two Lie subalgebras have equal underlying sets, then the application of the equivalence to an element x yields the same x after transporting along the equality.

Русский

Если два подалгебра Ли имеют одинаковые множества, применение эквивалента к элементу x возвращает x после перенесения по равенству.

LaTeX

$$$(\\uparrow(\\text{ofEq } L L' h x) : L) = x$$$

Lean4

@[simp]
theorem ofEq_apply (L L' : LieSubalgebra R L₁) (h : (L : Set L₁) = L') (x : L) : (↑(ofEq L L' h x) : L₁) = x :=
  rfl

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