English
For any index type ι, if each R_i is a topological semiring, then the function type ∀ i, R_i is a topological semiring.
Русский
Для любого типа индекса ι, если каждый R_i — топологическое полукольцо, то ∀ i, R_i — топологическое полукольцо.
LaTeX
$$IsTopologicalSemiring (∀ i, R i)$$
Lean4
theorem of_nhds_zero (hadd : Tendsto (uncurry ((· + ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
(hneg : Tendsto (fun x => -x : R → R) (𝓝 0) (𝓝 0))
(hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
(hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
(hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0)
(hleft : ∀ x₀ : R, 𝓝 x₀ = map (fun x => x₀ + x) (𝓝 0)) : IsTopologicalRing R :=
have := IsTopologicalAddGroup.of_comm_of_nhds_zero hadd hneg hleft
IsTopologicalRing.of_addGroup_of_nhds_zero hmul hmul_left hmul_right
