English
For any x ≠ ∞, the neighborhoods of x have a basis given by closed intervals Icc(x−ε, x+ε) with ε ≠ 0.
Русский
При x ≠ ∞ окрестности x имеют базис из замкнутых интервалов Icc(x−ε, x+ε) с ε ≠ 0.
LaTeX
$$$\\text{HasBasis} (\\cdot \\neq 0) (ε \\mapsto Icc(x-ε, x+ε))$ for $xt$ with $xt: x \\neq ∞$$$
Lean4
/-- Closed intervals `Set.Icc (x - ε) (x + ε)`, `ε ≠ 0`, form a basis of neighborhoods of an
extended nonnegative real number `x ≠ ∞`. We use `Set.Icc` instead of `Set.Ioo` because this way the
statement works for `x = 0`.
-/
theorem hasBasis_nhds_of_ne_top' (xt : x ≠ ∞) : (𝓝 x).HasBasis (· ≠ 0) (fun ε => Icc (x - ε) (x + ε)) :=
by
rcases (zero_le x).eq_or_lt with rfl | x0
· simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
exact nhds_bot_basis_Iic
· refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
· rintro ⟨a, b⟩ ⟨ha, hb⟩
rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
· exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
· exact (add_le_add_left (min_le_right _ _) _).trans_lt hδ
· exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0, lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩
