English
If L is a left-sided neighborhood and R a right-sided neighborhood of b, then (L ∩ (-∞, b]) ∪ (R ∩ [b, ∞)) is a neighborhood of b.
Русский
Если L является окрестностью слева, а R окрестностью справа точки b, то (L ∩ ≤b) ∪ (R ∩ ≥b) является окрестностью b.
LaTeX
$$$$ (L \\cap Iic(b)) \\cup (R \\cap Ici(b)) \\in 𝓝(b) $$$$
Lean4
/-- Obtain a "predictably-sided" neighborhood of `b` from two one-sided neighborhoods. -/
theorem nhds_of_Ici_Iic [LinearOrder α] {b : α} {L : Set α} (hL : L ∈ 𝓝[≤] b) {R : Set α} (hR : R ∈ 𝓝[≥] b) :
L ∩ Iic b ∪ R ∩ Ici b ∈ 𝓝 b :=
union_mem_nhds_of_mem_nhdsWithin Iic_union_Ici.symm (inter_mem hL self_mem_nhdsWithin)
(inter_mem hR self_mem_nhdsWithin)
