English
Let X and Y be partially ordered spaces. For x = (a,b) in X × Y, if the left-neighborhoods (nhdsWithin a in (-∞, a)) and (nhdsWithin b in (-∞, b)) are nonempty, then the left-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 instNeBotNhdsWithinIio [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⟩
