α : Type u
β : Type v
inst✝ : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x, x ∈ t ∧ ↑l ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x, x ∈ s ∪ t ∧ ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x, x ∈ s ∪ t ∧ ↑l ≤ 𝓝 x)
α : Type u
β : Type v
inst✝ : UniformSpace α
s t : Set α
hs : IsComplete s
ht : IsComplete t
⊢ IsComplete (s ∪ t)
simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *
no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x, x ∈ t ∧ ↑l ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x, x ∈ s ∪ t ∧ ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x, x ∈ s ∪ t ∧ ↑l ≤ 𝓝 x)
exact fun l hl =>
  ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
    (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩