English
For a finite index set with linear orders, if all left and right bounds hold (a_i < x_i and x_i < b_i), then the box Icc(a,b) is a neighborhood of x.
Русский
Для конечного индекса и линейных порядков, если каждая пара границ удовлетворяет a_i < x_i < b_i, то Icc(a,b) является окрестностью x.
LaTeX
$$Icc a' b' ∈ 𝓝 x' when ∀ i, a'_i < x'_i and ∀ i, x'_i < b'_i$$
Lean4
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated above from `f x` is countable. -/
theorem countable_image_lt_image_Iio [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
Set.Countable {x | ∃ z, f x < z ∧ ∀ y, y < x → z ≤ f y} :=
countable_image_lt_image_Ioi (β := βᵒᵈ) f
