English
With ε>0, a subset s of (Sum X Y)×(Sum X Y) belongs to the uniformity of X⊕Y exactly when there is δ>0 such that glueDist Φ Ψ ε a b < δ implies (a,b)∈s for all a,b in Sum X Y.
Русский
Для ε>0, множество s ⊆ (Sum X Y)×(Sum X Y) принадлежит униформности суммы X⊕Y тогда и только тогда, когда существует δ>0 такое, что glueDist Φ Ψ ε a b < δ влечет (a,b)∈s для всех a,b∈Sum X Y.
LaTeX
$$$ s \in 𝓤( X \oplus Y) \iff ∃ δ>0, ∀ a,b,\ glueDist Φ Ψ ε a b < δ \Rightarrow (a,b) ∈ s. $$$
Lean4
theorem mem_uniformity_iff_glueDist (hε : 0 < ε) (s : Set ((X ⊕ Y) × (X ⊕ Y))) :
s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ a b, glueDist Φ Ψ ε a b < δ → (a, b) ∈ s :=
by
simp only [Sum.uniformity, Filter.mem_sup, Filter.mem_map, mem_uniformity_dist, mem_preimage]
constructor
· rintro ⟨⟨δX, δX0, hX⟩, δY, δY0, hY⟩
refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
rintro (a | a) (b | b) h <;> simp only [lt_min_iff] at h
· exact hX h.1.1
· exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt
· exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt
· exact hY h.1.2
· rintro ⟨ε, ε0, H⟩
constructor <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩
