equivOfEq_trans — Mathlib

English

For subalgebras S ⊆ T ⊆ U, the transitivity of equality yields a compatibility: (equivOfEq S T hST).trans (equivOfEq T U hTU) = equivOfEq S U (hST.trans hTU).

Русский

Для подпалгебр S ⊆ T ⊆ U справедливо: композиция эквивалентов равенств равна эквиваленту равенства S ∼ U через транситивность.

LaTeX

$$$\bigl(\text{equivOfEq } S T hST\bigr).\text{trans} (\text{equivOfEq } T U hTU) = \text{equivOfEq } S U (hST.trans hTU)$$$

Lean4

@[simp]
theorem equivOfEq_trans (S T U : Subalgebra R A) (hST : S = T) (hTU : T = U) :
    (equivOfEq S T hST).trans (equivOfEq T U hTU) = equivOfEq S U (hST.trans hTU) :=
  rfl

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