toSubsemiring_le_toSubsemiring — Mathlib

English

For RingPreorder P1, P2, P1.toSubsemiring ≤ P2.toSubsemiring iff P1 ≤ P2.

Русский

Для RingPreordering P1, P2 верна эквивалентность: P1.toSubsemiring ≤ P2.toSubsemiring тогда и только тогда, когда P1 ≤ P2.

LaTeX

$$$P_1^{{\\mathrm{subsemiring}}} \\le P_2^{{\\mathrm{subsemiring}}} \\iff P_1 \\le P_2$$$

Lean4

theorem toSubsemiring_le_toSubsemiring {P₁ P₂ : RingPreordering R} : P₁.toSubsemiring ≤ P₂.toSubsemiring ↔ P₁ ≤ P₂ :=
  .rfl

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