toSubsemiring_lt_toSubsemiring

Mathlib.Algebra.Order.Ring.Ordering.Basic

URI: https://scilib.ai/kg/mathlib#RingPreordering.toSubsemiring_lt_toSubsemiring

English

P1.toSubsemiring < P2.toSubsemiring iff P1 < P2.

Русский

P1.toSubsemiring < P2.toSubsemiring тогда и только тогда, когда P1 < P2.

LaTeX

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

Lean4

theorem toSubsemiring_lt_toSubsemiring {P₁ P₂ : RingPreordering R} : P₁.toSubsemiring < P₂.toSubsemiring ↔ P₁ < P₂ :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru