coe_inducedOrderRingIso — Mathlib

English

The underlying function of the induced order ring isomorphism equals the induced map: the mapping function of inducedOrderRingIso β γ is exactly inducedMap β γ.

Русский

Функция, лежащая в основе индуцированного упорядоченного кольцевого изоморфизма β → γ, равна индуцированной карте: коeinducedOrderRingIso β γ = inducedMap β γ.

LaTeX

$$$ (\text{inducedOrderRingIso } \beta \gamma)^{\toFun} = \operatorname{inducedMap} \beta \gamma $$$

Lean4

@[simp]
theorem coe_inducedOrderRingIso : ⇑(inducedOrderRingIso β γ) = inducedMap β γ :=
  rfl

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