English
If α and β are star-ordered rings, then their product α × β, with the product order, is a star-ordered ring.
Русский
Если α и β — звездно упорядоченные кольца, то произведение α × β, упорядочение по компонентам, образует звёздно упорядоченное кольцо.
LaTeX
$$$$ \text{StarOrderedRing}(\alpha \times \beta) $$$$
Lean4
instance instStarOrderedRing [NonUnitalSemiring α] [NonUnitalSemiring β] [PartialOrder α] [PartialOrder β] [StarRing α]
[StarRing β] [StarOrderedRing α] [StarOrderedRing β] : StarOrderedRing (α × β) where
le_iff :=
Prod.forall.2 fun xa xy =>
Prod.forall.2 fun ya yb =>
by
have :
closure (Set.range fun s : α × β ↦ star s * s) =
(closure <| Set.range fun s : α ↦ star s * s).prod (closure <| Set.range fun s : β ↦ star s * s) :=
by
rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩), Set.prod_range_range_eq]
simp_rw [Prod.mul_def, Prod.star_def]
simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this, AddSubmonoid.mem_prod,
exists_and_exists_comm, and_and_and_comm]
