addOppositeEquiv_orderTop — Mathlib

English

The orderTop is preserved under the addOppositeEquiv map.

Русский

OrderTop сохраняется под отображением addOppositeEquiv.

LaTeX

$$$$ (addOppositeEquiv x).orderTop = x.orderTop. $$$$

Lean4

@[simp]
theorem addOppositeEquiv_orderTop (x : HahnSeries Γ Rᵃᵒᵖ) : (addOppositeEquiv x).unop.orderTop = x.orderTop := by
  classical
  simp only [orderTop, addOppositeEquiv_support]
  simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
  simp_rw [HahnSeries.ext_iff, funext_iff]
  simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

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