English
Characterizes openness in the disjoint union metric: a set is open iff every point has a positive radius ball contained in the set.
Русский
Характеризует открытость в метрическом пространстве дизъюнктивного объединения: множество открыто тогда и только тогда, когда каждая точка имеет положительный шар, полностью содержащий множество.
LaTeX
$$$\text{IsOpen}(s) \iff \forall x\in s,\; \exists \varepsilon>0,\; \forall y,\; \mathrm{dist}(x,y)<\varepsilon \Rightarrow y\in s$$$
Lean4
protected theorem isOpen_iff (s : Set (Σ i, E i)) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s :=
by
constructor
· rintro hs ⟨i, x⟩ hx
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s := Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
refine ⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩
rintro ⟨j, y⟩ hy
rcases eq_or_ne i j with (rfl | hij)
· simp only [Sigma.dist_same, lt_min_iff] at hy
exact hε (mem_ball'.2 hy.1)
· apply (lt_irrefl (1 : ℝ) _).elim
calc
1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
_ < 1 := hy.trans_le (min_le_right _ _)
· refine fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s := H ⟨i, x⟩ hx
refine ⟨ε, εpos, fun y hy => ?_⟩
apply hε ⟨i, y⟩
rw [Sigma.dist_same]
exact mem_ball'.1 hy
