English
Let ι be finite and each π(i) be a preordered topological space with the BoundedLENhdsClass property. Then the Pi-type ∀ i, π(i) (the product space) also has BoundedLENhdsClass.
Русский
Пусть ι конечно и для каждого i ∈ ι пространство π(i) является упорядоченным топологическим пространством с свойством BoundedLENhdsClass. Тогда произведение ∀ i, π(i) имеет то же свойство.
LaTeX
$$$ [\text{Finite } ι] \, [\forall i, Preorder (π i)] \, [\forall i, TopologicalSpace (π i)] \, [\forall i, BoundedLENhdsClass (π i)] \Rightarrow BoundedLENhdsClass (∀ i, π i). $$$
Lean4
instance instBoundedLENhdsClass [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
[∀ i, BoundedLENhdsClass (π i)] : BoundedLENhdsClass (∀ i, π i) :=
by
refine ⟨fun x ↦ ?_⟩
rw [nhds_pi]
choose f hf using fun i ↦ isBounded_le_nhds (x i)
exact ⟨f, eventually_pi hf⟩
