English
The product α × β inherits the boundedLENhds property from α and β; in particular, there is a canonical bound for nhds on the product.
Русский
Произведение пространств α×β обладает свойством boundedLENhds, полученным из α и β.
LaTeX
$$$$ \text{BoundedLENhdsClass }(\alpha \times \beta). $$$$
Lean4
/-- If `a > 1`, then open intervals `(a / ε, aε)`, `1 < ε ≤ a`,
form a basis of neighborhoods of `a`.
This upper bound for `ε` guarantees that all elements of these intervals are greater than one. -/
@[to_additive /-- If `a` is positive, then the intervals `(a - ε, a + ε)`, `0 < ε ≤ a`,
form a basis of neighborhoods of `a`.
This upper bound for `ε` guarantees that all elements of these intervals are positive. -/
]
theorem nhds_basis_Ioo_one_lt_of_one_lt [NoMaxOrder α] {a : α} (ha : 1 < a) :
(𝓝 a).HasBasis (fun ε : α => (1 : α) < ε ∧ ε ≤ a) fun ε => Ioo (a / ε) (a * ε) :=
(nhds_basis_Ioo_one_lt a).restrict fun ε hε ↦
⟨min a ε, lt_min ha hε, min_le_left _ _, by gcongr <;> apply min_le_right⟩
