α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
⊢ IsComplete S
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
⊢ IsComplete (⋃ (i : ι), s i)
set S := ⋃ i, s i
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 S
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
⊢ IsComplete S
intro l hl hls
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 S
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
rw [le_principal_iff] at hls
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
cases' cauchy_iff.1 hl with hl_ne hl'
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
  rcases hl' U hU with ⟨t, htl, htU⟩
  exact ⟨t ∩ S, inter_subset_right _ _, inter_mem htl hls,
    (Set.prod_mono (inter_subset_left _ _) (inter_subset_left _ _)).trans htU⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
  rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
  rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
  refine' ⟨i, fun y hy => _⟩
  rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
  rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
x : α
hxs : x ∈ s i
hlx : l ≤ 𝓝 x
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
x : α
hxs : x ∈ s i
hlx : l ≤ 𝓝 x
⊢ ∃ x, x ∈ S ∧ l ≤ 𝓝 x
exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
⊢ ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U
rcases hl' U hU with ⟨t, htl, htU⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U
exact ⟨t ∩ S, inter_subset_right _ _, inter_mem htl hls,
  (Set.prod_mono (inter_subset_left _ _) (inter_subset_left _ _)).trans htU⟩
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
⊢ ∃ i, t ⊆ s i
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ i, t ⊆ s i
rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
⊢ ∃ i, t ⊆ s i
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
⊢ ∃ i, t ⊆ s i
rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
⊢ y ∈ s i
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
⊢ ∃ i, t ⊆ s i
refine' ⟨i, fun y hy => _⟩
case intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s i
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
⊢ y ∈ s i
rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : Set (α × α)
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : NeBot l
hl' : ∀ (s : Set (α × α)), s ∈ 𝓤 α → ∃ t, t ∈ l ∧ t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s i
rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]