English
The product of a family of ordered rings is an ordered ring.
Русский
Произведение семейства упорядоченных колец является упорядочным кольцом.
LaTeX
$$$\\prod_{i\\in I} f_i\\text{ is an ordered ring when each } f_i\\text{ is ordered.}$$$
Lean4
instance isOrderedRing [∀ i, Semiring (f i)] [∀ i, PartialOrder (f i)] [∀ i, IsOrderedRing (f i)] :
IsOrderedRing (∀ i, f i)
where
add_le_add_left _ _ hab _ := fun _ => add_le_add_left (hab _) _
zero_le_one := fun i => zero_le_one (α := f i)
mul_le_mul_of_nonneg_left _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_left (hab _) <| hc _
mul_le_mul_of_nonneg_right _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_right (hab _) <| hc _
