mono — Mathlib

English

If x ≤ y and x is self-adjoint, then y is self-adjoint as well.

Русский

Если x ≤ y и x самоадъюнктно (самосопряжён), то и y является самосопряжённым.

LaTeX

$$$x \le y \land \star x = x \Rightarrow \star y = y$$$

Lean4

theorem mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y :=
  by
  rw [StarOrderedRing.le_iff] at h
  obtain ⟨d, hd, rfl⟩ := h
  rw [IsSelfAdjoint, star_add, hx.star_eq]
  congr
  refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd
  rintro - ⟨s, rfl⟩
  simp

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