English
Let X and Y be partially ordered spaces. For x = (a,b) in X × Y, if the right-neighborhoods (nhdsWithin a in (a, ∞)) and (nhdsWithin b in (b, ∞)) are nonempty, then the right-neighborhood of (a,b) is nonempty.
Русский
Пусть X и Y — частично упорядоченные пространства. Для x = (a,b) в X × Y, если правые окрестности (nhdsWithin a в (a, ∞)) и (nhdsWithin b в (b, ∞)) непусты, то правая окрестность (a,b) непуста.
LaTeX
$$$ (\\mathcal{N}_{>}(x_{1})).NeBot \\land (\\mathcal{N}_{>}(x_{2})).NeBot \\Rightarrow (\\mathcal{N}_{>}(x_{1}, x_{2})).NeBot $$$
Lean4
instance instNeBotNhdsWithinIoi [Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (𝓝[>] x.1).NeBot]
[hx₂ : (𝓝[>] x.2).NeBot] : (𝓝[>] x).NeBot :=
by
refine (hx₁.prod hx₂).mono ?_
rw [← nhdsWithin_prod_eq]
exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩
